On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep

WG211/M25Kammar: Revision history

From WG 2.11
Jump to navigationJump to search

Diff selection: Mark the radio buttons of the revisions to compare and hit enter or the button at the bottom.
Legend: (cur) = difference with latest revision, (prev) = difference with preceding revision, m = minor edit.

3 November 2025

  • curprev 18:2518:25, 3 November 2025 Jacques talk contribs 492 bytes +492 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..."
Retrieved from "http://mw.hh.se/wg211/index.php?title=WG211/M25Kammar"