New pages

11:1711:17, 26 October 2026 WG211/M26Yallop (hist | edit) [392 bytes] Jeremy-y (talk | contribs) (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.") Tag: Visual edit

07:5207:52, 13 October 2026 WG211/M26Kammar (hist | edit) [515 bytes] Ohad (talk | contribs) (Created page with "'''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''' ''Ohad Kammar'', joint work with ''Amaury Mazoyer''")

20:5120:51, 9 October 2026 WG211/M26Balaci (hist | edit) [985 bytes] Jacques (talk | contribs) (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...")
20:0820:08, 9 October 2026 WG211/M26Mullanix (hist | edit) [484 bytes] Jacques (talk | contribs) (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...")

09:0709:07, 7 October 2026 WG211/M26Kovacs (hist | edit) [905 bytes] Jeremy-y (talk | contribs) (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...") Tag: Visual edit

11:2911:29, 5 October 2026 WG211/M26Shan (hist | edit) [1,073 bytes] Jeremy-y (talk | contribs) (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...") Tag: Visual edit

Navigation menu