User contributions for Jacques

From WG 2.11
A user with 259 edits. Account created on 23 May 2012.
Jump to navigationJump to search
Search for contributionsExpandCollapse
⧼contribs-top⧽
⧼contribs-date⧽
(newest | oldest) View (newer 50 | ) (20 | 50 | 100 | 250 | 500)

12 October 2026

9 October 2026

  • 20:5120:51, 9 October 2026 diff hist +985 N 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..." current
  • 20:5120:51, 9 October 2026 diff hist +47 WG211/M26Schedule →Talks
  • 20:0820:08, 9 October 2026 diff hist +484 N 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..." current
  • 20:0820:08, 9 October 2026 diff hist +114 WG211/M26Schedule →Talks

7 October 2026

2 September 2026

24 August 2026

21 August 2026

13 June 2026

12 June 2026

5 June 2026

11 December 2025

  • 14:4014:40, 11 December 2025 diff hist +880 N 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..." current

10 December 2025

3 December 2025

2 December 2025

1 December 2025

21 November 2025

19 November 2025

12 November 2025

10 November 2025

7 November 2025

  • 17:0717:07, 7 November 2025 diff hist +760 N 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..." current
  • 17:0717:07, 7 November 2025 diff hist +88 WG211/M25Schedule →Talks and Schedule

3 November 2025

  • 18:2518:25, 3 November 2025 diff hist +492 N 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..." current
(newest | oldest) View (newer 50 | ) (20 | 50 | 100 | 250 | 500)