{"batchcomplete":"","continue":{"lecontinue":"20251210142942|1413","continue":"-||"},"query":{"logevents":[{"logid":1423,"ns":0,"title":"WG211/M26Yallop","pageid":705,"logpage":705,"revid":2938,"params":{},"type":"create","action":"create","user":"Jeremy-y","timestamp":"2026-10-26T10:17:18Z","comment":"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.\u00a0 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.\""},{"logid":1422,"ns":0,"title":"WG211/M26Bodo","pageid":704,"logpage":704,"revid":2934,"params":{},"type":"create","action":"create","user":"Sven-Bodo","timestamp":"2026-10-14T08:22:47Z","comment":"added abstract"},{"logid":1421,"ns":0,"title":"WG211/M26Kammar","pageid":703,"logpage":703,"revid":2926,"params":{},"type":"create","action":"create","user":"Ohad","timestamp":"2026-10-13T06:52:41Z","comment":"Created page with \"'''Modular construction of sound-and-complete simplifiers for varieties of semi-rings'''  ''Ohad Kammar'', joint work with ''Amaury Mazoyer''\""},{"logid":1420,"ns":0,"title":"WG211/M26Balaci","pageid":702,"logpage":702,"revid":2920,"params":{},"type":"create","action":"create","user":"Jacques","timestamp":"2026-10-09T19:51:54Z","comment":"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...\""},{"logid":1419,"ns":0,"title":"WG211/M26Mullanix","pageid":701,"logpage":701,"revid":2918,"params":{},"type":"create","action":"create","user":"Jacques","timestamp":"2026-10-09T19:08:54Z","comment":"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...\""},{"logid":1418,"ns":0,"title":"WG211/M26Kovacs","pageid":700,"logpage":700,"revid":2906,"params":{},"type":"create","action":"create","user":"Jeremy-y","timestamp":"2026-10-07T08:07:44Z","comment":"Created page with \"'''Thinning-stable metaprogramming'''  ''Andr\u00e1s Kov\u00e1cs''   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 \"\u2200 \u0393. Code \u0393 a \u2192 Code \u0393 b\". However, functions of suc...\""},{"logid":1417,"ns":0,"title":"WG211/M26Shan","pageid":699,"logpage":699,"revid":2902,"params":{},"type":"create","action":"create","user":"Jeremy-y","timestamp":"2026-10-05T10:29:48Z","comment":"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...\""},{"logid":1416,"ns":0,"title":"WG211/M26Schedule","pageid":698,"logpage":698,"revid":2873,"params":{},"type":"create","action":"create","user":"Jacques","timestamp":"2026-06-05T18:15:32Z","comment":"Created page with \"= IFIP Working Group 2.11, Twenty-sixth Meeting =  == 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.  === Venue...\""},{"logid":1415,"ns":0,"title":"W211/M25Shan","pageid":697,"logpage":697,"revid":2870,"params":{},"type":"create","action":"create","user":"Jacques","timestamp":"2025-12-11T13:40:31Z","comment":"Created page with \"Yafei Yang and Chung-chieh Shan  Developing quantum programs requires not only running them on quantum hardware but also simulating them on classical hardware. Because the semantics of a quantum program can be defined in terms of complex state vectors, it can in principle be simulated using any implementation of probabilistic or weighted programming that supports complex or at least negative weights. In this study, we compile a high-level quantum programming language to...\""},{"logid":1414,"ns":6,"title":"File:WG211 M25 Shan.pdf","pageid":696,"logpage":696,"revid":2869,"params":{},"type":"create","action":"create","user":"Jacques","timestamp":"2025-12-10T14:29:43Z","comment":""}]}}