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]]

WG 2.11 - Recent changes [en]

WG211/M26Yallop

WG211/M26Schedule