Main public logs

Combined display of all available logs of WG 2.11. You can narrow down the view by selecting a log type, the username (case-sensitive), or the affected page (also case-sensitive).

• 11:17, 26 October 2026 Jeremy-y talk contribs created page WG211/M26Yallop (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
• 09:22, 14 October 2026 Sven-Bodo talk contribs created page WG211/M26Bodo (added abstract)
• 07:52, 13 October 2026 Ohad talk contribs created page WG211/M26Kammar (Created page with "'''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''' ''Ohad Kammar'', joint work with ''Amaury Mazoyer''")
• 20:51, 9 October 2026 Jacques talk contribs created page WG211/M26Balaci (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:08, 9 October 2026 Jacques talk contribs created page WG211/M26Mullanix (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:07, 7 October 2026 Jeremy-y talk contribs created page WG211/M26Kovacs (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:29, 5 October 2026 Jeremy-y talk contribs created page WG211/M26Shan (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
• 19:15, 5 June 2026 Jacques talk contribs created page WG211/M26Schedule (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...")
• 14:40, 11 December 2025 Jacques talk contribs created page W211/M25Shan (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...")
• 15:29, 10 December 2025 Jacques talk contribs created page File:WG211 M25 Shan.pdf
• 15:29, 10 December 2025 Jacques talk contribs uploaded File:WG211 M25 Shan.pdf
• 15:26, 10 December 2025 Jacques talk contribs created page File:WG211 M25 Group Photo.jpg (Pictures of all the people who attended this meeting)
• 15:26, 10 December 2025 Jacques talk contribs uploaded File:WG211 M25 Group Photo.jpg (Pictures of all the people who attended this meeting)
• 09:17, 1 December 2025 Eric talk contribs created page File:Stellenbosch.pdf
• 09:17, 1 December 2025 Eric talk contribs uploaded File:Stellenbosch.pdf
• 20:13, 21 November 2025 Jacques talk contribs created page WG211/M25Barke (Created page with "Toward Trustworthy LLM Generation: From Verifiable Proofs to Reliable Agents Verifiable programming provides a concrete foundation for trustworthy LLM generation. This talk introduces DeepProof-32B, a 32-billion-parameter reasoning model designed for program verification and trained with reinforcement learning from verifiable rewards, achieving state-of-the-art performance among open models. The first part distills lessons from building models that can reason about thei...")
• 17:47, 19 November 2025 Jacques talk contribs created page WG211/M25Steuwer (Created page with "E-Graphs are a core data structure used in automatic reasoning and program optimization. They space-efficiently represent a set of equivalent terms. However, representing programs with bindings in e-graphs using existing techniques quickly defeats the efficiency purpose in many practical applications, as the e-graph represents alpha-equivalent terms many times. In this talk, I am going to present our work on Slotted E-Graphs that augment E-Graphs with a build-in notion...")
• 07:52, 18 November 2025 Maintenance script talk contribs changed group membership for Peoadmin from (none) to administrator, bureaucrat and interface administrator
• 07:52, 18 November 2025 User account Peoadmin talk contribs was created automatically
• 17:51, 10 November 2025 Bernd talk contribs created page WG211/M25Murase (Created page with "Kiselyov et al. introduced the notion of refined environment classifiers, which ensure scope-safe code generation with mutable state by annotating code types with *classifiers* that record the scoping information of code fragments. While their proposal was developed for a two-level, combinator-based code-generation language, we adapt their idea to quasi-quotation-based multi-stage programming in the style of MetaML. The resulting language guarantees scope-safe code gene...") Tag: Visual edit
• 17:50, 10 November 2025 Bernd talk contribs created page WG211/M25Lundquist (Created page with "Kiselyov et al. introduced the notion of refined environment classifiers, which ensure scope-safe code generation with mutable state by annotating code types with *classifiers* that record the scoping information of code fragments. While their proposal was developed for a two-level, combinator-based code-generation language, we adapt their idea to quasi-quotation-based multi-stage programming in the style of MetaML. The resulting language guarantees scope-safe code ge...")
• 17:07, 7 November 2025 Jacques talk contribs created page WG211/M25Yallop (Created page with "(joint work with Guillaume Allais, Edwin Brady, Nathan Corbyn and Ohad Kammar) We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library's dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well...")
• 18:25, 3 November 2025 Jacques talk contribs created page WG211/M25Kammar (Created page with "I will describe work in progress implementing SMTLIB bindings in Idris 2. The bindings are well-scoped and intrinsically typed, and support holes and type-and-scope-safe splicing of query fragments. Since SMTLIB describes upwards of 20 different combinations of features, this is an instance of the Expression Problem. To work around it, we develop the modular abstract syntax trees (MAST) library. It provides generic, type and scope safe traversals of splicing of code frag...")
• 19:23, 31 October 2025 Jacques talk contribs created page WG211/M25Carette (Created page with "Notions of derivative abound in functional programming. An obvious question arises: what about integrals? It turns out that folds are the analogous concept. Pursuing the analogy leads us to a proper notion of "definite fold" corresponding to definite integrals (and sums and products and ...). Many concepts are needed along the way (Route, Pointed type, etc). In return, incremental and parallel versions of fold arise naturally. The correct notion of indefinite fold is a l...")
• 18:10, 5 December 2024 Jeremy-g talk contribs uploaded File:Wg211-20241202.pdf (Slides for "Continuation-Passing Style, Defunctionalization, Accumulations, and Associativity".)
• 20:23, 21 November 2024 Jeremy-y talk contribs moved page WG21//M24Kuper to WG211/M24Kuper
• 02:47, 13 November 2024 User account Friedrich talk contribs was created by Jacques talk contribs (Because plain users can't seem to on their own)
• 21:39, 3 October 2024 User account Sebastian talk contribs was created by Jacques talk contribs (new member)
• 21:57, 25 September 2024 User account Ohad talk contribs was created by Jacques talk contribs (Creating an account for Ohad)
• 00:45, 31 March 2024 Jeremy-y talk contribs uploaded File:Ballantyne-slides.pdf
• 12:33, 30 March 2024 Jeremy-y talk contribs uploaded File:Kellogg-slides.pdf
• 22:55, 15 March 2024 Jeremy-y talk contribs moved page WG211/M23Kellogg Static Program Reduction via Specification Slicing to WG211/M23Kellogg
• 23:36, 9 March 2024 User account Nada talk contribs was created by Jacques talk contribs (Because Nada does not have permission to do it herself)
• 11:53, 28 April 2023 Jacques talk contribs uploaded File:Slides-delft-wg-2-11-partial-evaluation-algebra.pdf
• 21:32, 27 April 2023 Jacques talk contribs uploaded File:Fischer-Delft-GrammarRepair.pptx (Bernd's slides)
• 20:28, 27 April 2023 Jacques talk contribs uploaded File:DatalogDebugging.pdf (Sebastian's slides)
• 18:49, 27 April 2023 Jacques talk contribs uploaded File:Macros.pdf (Slides from Jeremy)
• 17:22, 8 April 2023 Jeremy-g talk contribs uploaded File:M22-Gibbons.pdf
• 19:30, 6 April 2023 Eric talk contribs uploaded File:M22-Van-Wyk-scopes-trees-graphs-dsls.pdf
• 09:10, 6 April 2023 Julia talk contribs uploaded File:Slides lawall m22.pdf (Slides)
• 18:40, 30 March 2023 Peter talk contribs uploaded File:Delft Mekelpark.jpeg
• 18:38, 30 March 2023 Peter talk contribs uploaded File:Delft 28.jpeg
• 18:38, 30 March 2023 Peter talk contribs uploaded File:Delft lunch room.jpeg
• 18:37, 30 March 2023 Peter talk contribs uploaded File:Delft lunch route 3.jpeg
• 18:37, 30 March 2023 Peter talk contribs uploaded File:Delft lunch route 2.jpeg
• 18:36, 30 March 2023 Peter talk contribs uploaded File:Delft lunch route 1.jpeg
• 18:35, 30 March 2023 Peter talk contribs uploaded File:Delft Timmanzaal.jpeg
• 18:35, 30 March 2023 Peter talk contribs uploaded File:Delft Lipkenszaal Timmanzaal.jpeg
• 18:34, 30 March 2023 Peter talk contribs uploaded File:Delft Snijderzaal.jpeg
• 18:33, 30 March 2023 Peter talk contribs uploaded File:Delft 36 climb.jpeg