WG 2.11 - Recent changes [en]

WG211/M26Yallop

Jeremy-y — Mon, 26 Oct 2026 10:17:18 GMT

Created page with "'''Staging with Equality''' ''Jeremy Yallop'' I present a study of the interaction between GADTs, typed quotations, and mutable state, and identify two classes of soundness problems. There are various static and dynamic checks that address the problems, and I discuss the application of those checks in the Modular Macros project and to the languages MetaOCaml, GHC Haskell, and Scala 3."

New page

'''Staging with Equality'''

''Jeremy Yallop''

I present a study of the interaction between GADTs, typed quotations, and mutable state, and identify two classes of soundness problems. There are various static and dynamic checks that address the problems, and I discuss the application of those checks in the Modular Macros project and to the languages MetaOCaml, GHC Haskell, and Scala 3.

WG211/M26Schedule

Jeremy-y — Mon, 26 Oct 2026 10:11:13 GMT

← Older revision		Revision as of 11:11, 26 October 2026
Line 69:		Line 69:
	* Satnam Singh "Bird-Meertens Style Derivation of Efficient Circuits from Specifications"		* Satnam Singh "Bird-Meertens Style Derivation of Efficient Circuits from Specifications"
	* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]		* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]
	* Jeremy Yallop "Staging with equality"		* Jeremy Yallop [[WG211/M26Yallop\|Staging with equality]]
	* Jason Balaci [[WG211/M26Balaci\|Generating Human-Readable Code]]		* Jason Balaci [[WG211/M26Balaci\|Generating Human-Readable Code]]
	* Reed Mullanix [[WG211/M26Mullanix\|Panbench: comparative benchmarking of proof assistants through parameterised program generation]]		* Reed Mullanix [[WG211/M26Mullanix\|Panbench: comparative benchmarking of proof assistants through parameterised program generation]]

WG211/M26Schedule

Igarashi — Thu, 15 Oct 2026 12:56:57 GMT

Schedule

← Older revision		Revision as of 13:56, 15 October 2026
(One intermediate revision by the same user not shown)
Line 117:		Line 117:
	** 09:45 - 10:30 Lawall		** 09:45 - 10:30 Lawall
	* 10:30 - 11:00 Coffee break		* 10:30 - 11:00 Coffee break
	** 11:00 - 11:45 ~~TBD~~		** 11:00 - 11:45 Mullanix
	** 11:45 - 12:30 ~~TBD~~		** 11:45 - 12:30 Toohey
	* 12:30 - 14:30 Lunch and break		* 12:30 - 14:30 Lunch and break
	** 14:30 - 22:00 Excursion (Niagara region, Falls, Skylon Tower for dinner)		** 14:30 - 22:00 Excursion (Niagara region, Falls, Skylon Tower for dinner)
Line 124:		Line 124:
	Friday, October 16		Friday, October 16
	* 08:30 - 09:15 Breakfast		* 08:30 - 09:15 Breakfast
	** 09:15 - 10:00 ~~TBD~~		** 09:15 - 10:00 Scholz
	** 10:00 - 10:45 ~~TBD~~		** 10:00 - 10:45 Yallop
	* 10:45 - 11:15 Coffee break		* 10:45 - 11:15 Coffee break
	** 11:15 - 12:00 ~~TBD~~		** 11:15 - 12:00 Igarashi
	* 12:00 - 13:30 Lunch and end of meeting		* 12:00 - 13:30 Lunch and end of meeting

WG211/M26Bodo

Sven-Bodo — Wed, 14 Oct 2026 08:22:47 GMT

added abstract

New page

'''Code Generation in the Mirror --- on Generating ONNX for Scientific Codes'''

'''Sven-Bodo Scholz'''

Many new architectures have been created aiming at improved AI computations.
These machines promise faster computations or lower power consumption in comparison to standard hardware.
Given that AI computations are mainly based on a small set of linear algebra operations it should be possible to
leverage the benefits of these architectures for scientific computation as well. In a first attempt to do so, we look into
the feasibility of leveraging Open Neural Network Exchange (ONNX) as an intermediate representation which
is supported by a rather wide range of accelerator platforms.

The key challenge here is that ONNX is on a rather high level of abstraction which seems to to turn the code generation task
into a code analysis task. This talk presents an idea to address this analysis task by a combination of functional abstraction
and ONNX code generation. We present our first experiences when turning scientific applications written in SaC into ONNX programs.

WG211/M26Schedule

Sven-Bodo — Wed, 14 Oct 2026 07:59:22 GMT

Talks

← Older revision		Revision as of 08:59, 14 October 2026
(One intermediate revision by the same user not shown)
Line 60:		Line 60:
	The following people have confirmed they will giving a talk:		The following people have confirmed they will giving a talk:

	* Sven-Bodo Scholz ~~TBD~~		* Sven-Bodo Scholz [[WG211/M26Bodo\|Code Generation in the Mirror --- on Generating ONNX for Scientific Codes]]
	* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"		* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"
	* Ohad Kammar [[WG211/M26Kammar\|Modular construction of sound-and-complete simplifiers for varieties of semi-rings]] ([http://www.denotational.co.uk/talks/wg211-modular-distributivity.pdf slides])		* Ohad Kammar [[WG211/M26Kammar\|Modular construction of sound-and-complete simplifiers for varieties of semi-rings]] ([http://www.denotational.co.uk/talks/wg211-modular-distributivity.pdf slides])

WG211/M26Schedule

Igarashi — Wed, 14 Oct 2026 01:58:35 GMT

Schedule

← Older revision		Revision as of 02:58, 14 October 2026
(One intermediate revision by the same user not shown)
Line 100:		Line 100:

	* 08:30 - 09:15 Breakfast		* 08:30 - 09:15 Breakfast
	** 09:15 - 10:00 ~~TBD~~		** 09:15 - 10:00 Xie
	** 10:00 - 10:45 ~~TBD~~		** 10:00 - 10:45 Barke
	* 10:45 - 11:15 Coffee break		* 10:45 - 11:15 Coffee break
	** 11:15 - 12:00 ~~TBD~~		** 11:15 - 12:00 Shaikhha
	* 12:00 - 13:30 Lunch and break		* 12:00 - 13:30 Lunch and break
	** 13:30 - 14:15 ~~TBD~~		** 13:30 - 14:15 Wei
	** 14:15 - 15:00 ~~TBD~~		** 14:15 - 15:00 Balaci
	* 15:00 - 15:45 Coffee break		* 15:00 - 15:45 Coffee break
	** 15:45 - 16:45 Business Meeting		** 15:45 - 16:45 Business Meeting
Line 114:		Line 114:
	Thursday, October 15		Thursday, October 15
	* 08:30 - 09:00 Breakfast		* 08:30 - 09:00 Breakfast
	** 09:00 - 09:45 ~~TBD~~		** 09:00 - 09:45 Singh
	** 09:45 - 10:30 ~~TBD~~		** 09:45 - 10:30 Lawall
	* 10:30 - 11:00 Coffee break		* 10:30 - 11:00 Coffee break
	** 11:00 - 11:45 TBD		** 11:00 - 11:45 TBD

WG211/M26Kammar

Ohad — Tue, 13 Oct 2026 06:58:59 GMT

← Older revision		Revision as of 07:58, 13 October 2026
Line 2:		Line 2:

	''Ohad Kammar'', joint work with ''Amaury Mazoyer''		''Ohad Kammar'', joint work with ''Amaury Mazoyer''

			We characterise the free models of a distributive combination of
			finitary algebraic theories in terms of free models for each combined
			theory, under suitable assumptions proposed by [https://doi.org/10.4230/LIPIcs.LICS.2026.45 Fuji etal. (2026)]. This characterisation leads to dozens of
			sound-and-complete algebraic simplifiers performant enough for
			rote-proof synthesis.

WG211/M26Schedule

Ohad — Tue, 13 Oct 2026 06:53:56 GMT

Talks

← Older revision		Revision as of 07:53, 13 October 2026
(One intermediate revision by the same user not shown)
Line 62:		Line 62:
	* Sven-Bodo Scholz TBD		* Sven-Bodo Scholz TBD
	* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"		* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"
	* Ohad Kammar ''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''		* Ohad Kammar [[WG211/M26Kammar\|Modular construction of sound-and-complete simplifiers for varieties of semi-rings]] ([http://www.denotational.co.uk/talks/wg211-modular-distributivity.pdf slides])
	* Julia Lawall: AI discussion		* Julia Lawall: AI discussion
	* Michael Adams "Fixen: A Fixed-Point Algorithm Generator"		* Michael Adams "Fixen: A Fixed-Point Algorithm Generator"

WG211/M26Kammar

Ohad — Tue, 13 Oct 2026 06:52:41 GMT

Created page with "'''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''' ''Ohad Kammar'', joint work with ''Amaury Mazoyer''"

New page

'''Modular construction of sound-and-complete simplifiers for varieties of semi-rings'''

''Ohad Kammar'', joint work with ''Amaury Mazoyer''

WG211/M26Schedule

Jacques — Mon, 12 Oct 2026 17:33:04 GMT

Schedule

← Older revision		Revision as of 18:33, 12 October 2026
(One intermediate revision by the same user not shown)
Line 80:		Line 80:

	== Schedule ==		== Schedule ==

			Tuesday, October 13

			* 08:30 - 09:00 Breakfast
			* 09:00 - 09:15 Welcome and organization
			** 09:15 - 10:00 Shan
			** 10:00 - 10:45 Steimann
			* 10:45 - 11:15 Coffee break
			** 11:15 - 12:00 Kammar
			* 12:00 - 13:30 Lunch and break
			** 13:30 - 14:15 Adams
			** 14:15 - 15:00 Harrison
			* 15:00 - 15:30 Coffee break
			** 15:30 - 16:15 Kovacs

			* 18:30 Leave for Dinner: [https://www.triuswines.com/ Trius Winery]

			Wednesday, October 14

			* 08:30 - 09:15 Breakfast
			** 09:15 - 10:00 TBD
			** 10:00 - 10:45 TBD
			* 10:45 - 11:15 Coffee break
			** 11:15 - 12:00 TBD
			* 12:00 - 13:30 Lunch and break
			** 13:30 - 14:15 TBD
			** 14:15 - 15:00 TBD
			* 15:00 - 15:45 Coffee break
			** 15:45 - 16:45 Business Meeting

			* 18:30 Leave for Dinner: [https://www.peller.com/ Peller Estates Winery]

			Thursday, October 15
			* 08:30 - 09:00 Breakfast
			** 09:00 - 09:45 TBD
			** 09:45 - 10:30 TBD
			* 10:30 - 11:00 Coffee break
			** 11:00 - 11:45 TBD
			** 11:45 - 12:30 TBD
			* 12:30 - 14:30 Lunch and break
			** 14:30 - 22:00 Excursion (Niagara region, Falls, Skylon Tower for dinner)

			Friday, October 16
			* 08:30 - 09:15 Breakfast
			** 09:15 - 10:00 TBD
			** 10:00 - 10:45 TBD
			* 10:45 - 11:15 Coffee break
			** 11:15 - 12:00 TBD
			* 12:00 - 13:30 Lunch and end of meeting

	== Travel ==		== Travel ==

WG211/M26Schedule

Ohad — Mon, 12 Oct 2026 07:23:34 GMT

Arrivals and departures of attendees

← Older revision		Revision as of 08:23, 12 October 2026
Line 122:		Line 122:

	Friedrich: I am scheduled to arrive on Oct 12th (Mon) at 12:50 pm (AC 0841), YYZ. Happy to share a ride, possibly public transport? (The trick will not work for me, because of deaparture times.) I wil leave on Friday, 18:20 (AC 9104)		Friedrich: I am scheduled to arrive on Oct 12th (Mon) at 12:50 pm (AC 0841), YYZ. Happy to share a ride, possibly public transport? (The trick will not work for me, because of deaparture times.) I wil leave on Friday, 18:20 (AC 9104)

			Ohad: For simplicity, I'm taking the Niagra Airbus. Arrival departing from Toronto International Airport on Monday, October 12, 2026 between 15:00 and 15:20, departure departing Friday, October 16, 2026 between 15:00 and 15:20. No idea if this can be shared, but perfectly happy to share with anyone who knows how to share it.

WG211/M26Schedule

Friedrich — Mon, 12 Oct 2026 06:17:37 GMT

Arrivals and departures of attendees: added aiport

← Older revision		Revision as of 07:17, 12 October 2026
Line 121:		Line 121:
	Bodo: I will arrive on Oct 13th, around 4pm; most likely by rental car from YYZ.		Bodo: I will arrive on Oct 13th, around 4pm; most likely by rental car from YYZ.

	Friedrich: I am scheduled to arrive on Oct 12th (Mon) at 12:50 pm (AC 0841). Happy to share a ride, possibly public transport? (The trick will not work for me, because of deaparture times.) I wil leave on Friday, 18:20 (AC 9104)		Friedrich: I am scheduled to arrive on Oct 12th (Mon) at 12:50 pm (AC 0841), YYZ. Happy to share a ride, possibly public transport? (The trick will not work for me, because of deaparture times.) I wil leave on Friday, 18:20 (AC 9104)

WG211/M26Schedule

Igarashi — Sun, 11 Oct 2026 09:52:50 GMT

Talks

← Older revision		Revision as of 10:52, 11 October 2026
Line 67:		Line 67:
	* Chung-chieh Shan [[WG211/M26Shan\|Formalizing einsum with named tensor notation]]		* Chung-chieh Shan [[WG211/M26Shan\|Formalizing einsum with named tensor notation]]
	* Harrison Goldstein "New Foundations for Property-Based Testing"		* Harrison Goldstein "New Foundations for Property-Based Testing"
	* Satnam Singh "~~Hardware Verification with an AI Theorem Prover~~"		* Satnam Singh "Bird-Meertens Style Derivation of Efficient Circuits from Specifications"
	* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]		* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]
	* Jeremy Yallop "Staging with equality"		* Jeremy Yallop "Staging with equality"

WG211/M26Balaci

Jacques — Fri, 09 Oct 2026 19:51:54 GMT

Created page with "Executable code often takes priority over documentation in software development. One inherent problem is knowledge duplication in code and documentation. Can we avoid that by generating everything? What would such a process look like? This talk will discuss exploratory work in Drasil, a software generation framework for complete scientific software artifacts fit for humans, where we define "complete" as containing all software artifacts normally contained in a code repo..."

New page

Executable code often takes priority over documentation in software development. One inherent problem is knowledge duplication in code and documentation. Can we avoid that by generating everything? What would such a process look like?

This talk will discuss exploratory work in Drasil, a software generation framework for complete scientific software artifacts fit for humans, where we define "complete" as containing all software artifacts normally contained in a code repository (code, documentation, build scripts, etc.), and "fit for humans" as being well-documented and being idiomatic with meaningful identifiers.

The software generation pipeline in Drasil resembles a highly rational, explainable software development process. This talk will deconstruct said process, discussing: codifying problem-space concepts with domain-specific languages, refining problems into solutions through making concrete decisions about how problems should be translated into software artifacts.

WG211/M26Schedule

Jacques — Fri, 09 Oct 2026 19:51:20 GMT

Talks

← Older revision		Revision as of 20:51, 9 October 2026
Line 70:		Line 70:
	* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]		* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]
	* Jeremy Yallop "Staging with equality"		* Jeremy Yallop "Staging with equality"
	* Jason Balaci ~~TBD~~		* Jason Balaci [[WG211/M26Balaci\|Generating Human-Readable Code]]
	* Reed Mullanix [[WG211/M26Mullanix\|Panbench: comparative benchmarking of proof assistants through parameterised program generation]]		* Reed Mullanix [[WG211/M26Mullanix\|Panbench: comparative benchmarking of proof assistants through parameterised program generation]]
	* Atsushi Igarashi "Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types"		* Atsushi Igarashi "Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types"

WG211/M26Mullanix

Jacques — Fri, 09 Oct 2026 19:08:54 GMT

Created page with "Proof assistants based off of dependent types all use roughly the same core calculi, but use a variety of implementation strategies for their front-ends. To compare and constrast the performance of these systems, we have developed \emph{Panbench}, an extensible DSL for generating programs of increasing size for Agda 2, Rocq, Lean 4, and Idris 2. In this talk, I will discuss the design of the Panbench DSL, and detail a refinement of tagless embeddings used to encode it in..."

New page

Proof assistants based off of dependent types all use roughly the same
core calculi, but use a variety of implementation strategies for their
front-ends. To compare and constrast the performance of these systems,
we have developed \emph{Panbench}, an extensible DSL for generating programs
of increasing size for Agda 2, Rocq, Lean 4, and Idris 2. In this talk, I will
discuss the design of the Panbench DSL, and detail a refinement of tagless embeddings used to encode it in Haskell.

WG211/M26Schedule

Jacques — Fri, 09 Oct 2026 19:08:24 GMT

Talks

← Older revision		Revision as of 20:08, 9 October 2026
Line 71:		Line 71:
	* Jeremy Yallop "Staging with equality"		* Jeremy Yallop "Staging with equality"
	* Jason Balaci TBD		* Jason Balaci TBD
	* Reed Mullanix ~~TBD~~		* Reed Mullanix [[WG211/M26Mullanix\|Panbench: comparative benchmarking of proof assistants through parameterised program generation]]
	* Atsushi Igarashi "Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types"		* Atsushi Igarashi "Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types"
	* Ningning Xie (with Oghenevwogaga Ebresafe) "A Verified Compiler for Effect Handlers"		* Ningning Xie (with Oghenevwogaga Ebresafe) "A Verified Compiler for Effect Handlers"

WG211/M26Schedule

Igarashi — Fri, 09 Oct 2026 06:54:51 GMT

Talks

← Older revision		Revision as of 07:54, 9 October 2026
(3 intermediate revisions by the same user not shown)
Line 72:		Line 72:
	* Jason Balaci TBD		* Jason Balaci TBD
	* Reed Mullanix TBD		* Reed Mullanix TBD
			* Atsushi Igarashi "Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types"
			* Ningning Xie (with Oghenevwogaga Ebresafe) "A Verified Compiler for Effect Handlers"
			* Matthew Toohey "A Lean-Based Programming Language Specification Tool” (if time permits)
			* Shraddha Barke "Mining Symbolic Constraints for Tool-calling Agents" (14th or after?)
			* Amir Shaikhha "Einstein Meets Codd: Tensor Algebra through the Lens of Relational Algebra"
			* Guannan Wei "When Do Staging Annotations Preserve Semantics?" (14th or after?)

	== Schedule ==		== Schedule ==

WG211/M26Schedule

Jacques — Wed, 07 Oct 2026 19:27:30 GMT

Talks

← Older revision		Revision as of 20:27, 7 October 2026
(4 intermediate revisions by the same user not shown)
Line 3:		Line 3:
	== October 13-16, 2026, Niagara-on-the-Lake, Ontario, Canada ==		== October 13-16, 2026, Niagara-on-the-Lake, Ontario, Canada ==

	The meeting will be held on the (outskirts of) Niagara-on-the-Lake, in the middle of the Niagara region wine country, hosted by [mailto:carette@mcmaster.ca Jacques Carette]. The meeting is planned for 3.5 days, with a half day on October 16~~. More details, program, and registration information will be appearing on this page in the next few weeks~~.		The meeting will be held on the (outskirts of) Niagara-on-the-Lake, in the middle of the Niagara region wine country, hosted by [mailto:carette@mcmaster.ca Jacques Carette]. The meeting is planned for 3.5 days, with a half day on October 16.

	=== Venue ===		=== Venue ===

	The meeting will actually be held at a hotel (wineries were too expensive), the [https://www.hilton.com/en/hotels/xlvnlgi-hilton-garden-inn-niagara-on-the-lake/ Hilton Garden Inn]~~. Details to appear before June 10th~~. Be warned: the hotel itself is "in the middle of nowhere" (even though there are actually 3 hotels at that spot).		The meeting will actually be held at a hotel (wineries were too expensive), the [https://www.hilton.com/en/hotels/xlvnlgi-hilton-garden-inn-niagara-on-the-lake/ Hilton Garden Inn]. Be warned: the hotel itself is "in the middle of nowhere" (even though there are actually 3 hotels at that spot).

			Note that breakfast is included at the meeting itself.

	=== Group dinners ===		=== Group dinners ===

	Dinners will be arranged at winery-restaurants. It will ~~be necessary~~ to ~~take~~ a ~~(chartered~~) ~~bus to get there~~, as there is nothing within easy walking distance of the hotel. ~~Details will appear a couple~~ of ~~weeks before~~ the ~~event~~.		Dinners will be arranged at winery-restaurants. We will need to carpool (or hire a couple of taxis), as there is nothing within easy walking distance of the hotel.

			* Tuesday 13th: [https://www.triuswines.com/ Trius Winery]
			* Wednesday 14th: [https://www.peller.com/ Peller Estates Winery]
			* Thursday 15th: [https://www.skylon.com/ Skylon Tower Revolving Restaurant] (as part of the excursion); this is all about the view...

			Trius is not particularly far, but unfortunately the road there is a country road with no lighting and no sidewalk.

	=== Group excursion ===		=== Group excursion ===

	~~TBD~~.		Pick up at 2:30pm. We'll see some nice spots along the way, have a Maple syrup and chocolate tasting, a boat ride to the Falls, a bit of free time around Clifton Hill (the kitchy-touristy part of Niagara Falls), a guided tour of the Falls including 'Journey behind the Falls', dinner at 8:00 at Skylon Tower, with a 10pm departure back to the hotel.

	=== Registration fee ===		=== Registration fee ===

	Registration fee is ~~TBD~~.		Registration fee is can$1035. Details of how to pay were emailed out.

	=== Members attending ===		=== Members attending ===
Line 62:		Line 70:
	* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]		* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]
	* Jeremy Yallop "Staging with equality"		* Jeremy Yallop "Staging with equality"
			* Jason Balaci TBD
			* Reed Mullanix TBD

	== Schedule ==		== Schedule ==

WG211/M26Schedule

Jeremy-y — Wed, 07 Oct 2026 10:39:30 GMT

Talks

← Older revision		Revision as of 11:39, 7 October 2026
Line 61:		Line 61:
	* Satnam Singh "Hardware Verification with an AI Theorem Prover"		* Satnam Singh "Hardware Verification with an AI Theorem Prover"
	* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]		* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]
			* Jeremy Yallop "Staging with equality"

	== Schedule ==		== Schedule ==

WG211/M26Kovacs

Jeremy-y — Wed, 07 Oct 2026 08:07:44 GMT

Created page with "'''Thinning-stable metaprogramming''' ''András Kovács'' In this talk I give an overview of various notions of stability in metaprogramming and propose stability under thinning as a setup which shows some promise and which has not yet been explored. When we have "f : Code a -> Code b" in some staged language, we expect "f" to work on object expressions in arbitrary scopes. So, semantically we'd like to have "∀ Γ. Code Γ a → Code Γ b". However, functions of suc..."

New page

'''Thinning-stable metaprogramming'''

''András Kovács''

In this talk I give an overview of various notions of stability in metaprogramming and propose stability under thinning as a setup which shows some promise and which has not yet been explored. When we have "f : Code a -> Code b" in some staged language, we expect "f" to work on object expressions in arbitrary scopes. So, semantically we'd like to have "∀ Γ. Code Γ a → Code Γ b". However, functions of such type can inspect Γ in arbitrary unhygienic ways. So we'd like to restrict ourselves to metaprograms that are stable under certain morphisms between object-level scopes. Previous works have explored stability under a) substitution b) variable renaming c) injective variable renaming, in various logical frameworks and nominal and staged calculi. I investigate stability under thinning (also known as order-preserving embedding).

WG211/M26Schedule

Jeremy-y — Wed, 07 Oct 2026 08:07:10 GMT

Talks

← Older revision		Revision as of 09:07, 7 October 2026
(2 intermediate revisions by the same user not shown)
Line 46:		Line 46:
	* Matthew Toohey (local observer)		* Matthew Toohey (local observer)
	* Oghenevwogaga Ebresafe (local observer)		* Oghenevwogaga Ebresafe (local observer)
	* Harrison Goldstein		* Harrison Goldstein (local observer)

	== Talks ==		== Talks ==
Line 58:		Line 58:
	* Michael Adams "Fixen: A Fixed-Point Algorithm Generator"		* Michael Adams "Fixen: A Fixed-Point Algorithm Generator"
	* Chung-chieh Shan [[WG211/M26Shan\|Formalizing einsum with named tensor notation]]		* Chung-chieh Shan [[WG211/M26Shan\|Formalizing einsum with named tensor notation]]
			* Harrison Goldstein "New Foundations for Property-Based Testing"
			* Satnam Singh "Hardware Verification with an AI Theorem Prover"
			* András Kovács [[WG211/M26Kovacs\|Thinning-stable metaprogramming]]

	== Schedule ==		== Schedule ==

WG211/M26Shan

Jeremy-y — Mon, 05 Oct 2026 10:29:48 GMT

Created page with "'''Formalizing einsum with named tensor notation''' ''Yafei Yang and Chung-chieh Shan'', Indiana University Einstein notation (einsum) is a widely adopted tensor operation that has proven useful in areas such as machine learning and quantum computing. But it had no formal semantics until recently, and its properties had no mechanized verification. We formalize the denotational semantics of a language of tensors (multi-dimensional arrays) that supports einsum and repeat..."

New page

'''Formalizing einsum with named tensor notation'''

''Yafei Yang and Chung-chieh Shan'', Indiana University

Einstein notation (einsum) is a widely adopted tensor operation that has proven useful in areas such as machine learning and quantum computing. But it had no formal semantics until recently, and its properties had no mechanized verification. We formalize the denotational semantics of a language of tensors (multi-dimensional arrays) that supports einsum and repeated tensors (expand). With this semantics, we verify equational rewriting rules about einsum and expand that improve the performance of tensor computation. Whereas typical languages use unnamed tensors, whose shape is a sequence of natural numbers, we found it advantageous for mechanization to use named tensors, whose shape is a finite map from names to natural numbers. To our knowledge, this is the first time that the semantics and rewriting rules of einsum are mechanized in a proof assistant. Our solution is agnostic to proof assistants; we have implemented it in Lean and partially in Agda.

WG211/M26Schedule

Jeremy-y — Mon, 05 Oct 2026 10:29:25 GMT

Talks

← Older revision		Revision as of 11:29, 5 October 2026
(2 intermediate revisions by the same user not shown)
Line 56:		Line 56:
	* Ohad Kammar ''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''		* Ohad Kammar ''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''
	* Julia Lawall: AI discussion		* Julia Lawall: AI discussion
			* Michael Adams "Fixen: A Fixed-Point Algorithm Generator"
			* Chung-chieh Shan [[WG211/M26Shan\|Formalizing einsum with named tensor notation]]

	== Schedule ==		== Schedule ==

WG211/M26Schedule

Julia — Fri, 02 Oct 2026 17:20:58 GMT

Talks

← Older revision		Revision as of 18:20, 2 October 2026
Line 55:		Line 55:
	* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"		* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"
	* Ohad Kammar ''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''		* Ohad Kammar ''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''
			* Julia Lawall: AI discussion

	== Schedule ==		== Schedule ==

WG211/M26Schedule

Ohad — Tue, 29 Sep 2026 05:36:34 GMT

Talks: Add Ohad Kammar's talk title

← Older revision		Revision as of 06:36, 29 September 2026
Line 54:		Line 54:
	* Sven-Bodo Scholz TBD		* Sven-Bodo Scholz TBD
	* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"		* Friedrich Steimann "Types and modularity for implicit invocation with implicit announcement"
			* Ohad Kammar ''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''

	== Schedule ==		== Schedule ==