A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists
We show how types of finite sets and multisets can be constructed in ordinary dependent type theory, without the need for quotient types or working with setoids, and prove that these constructions realise finite sets and multisets as free idempotent commutative monoids and free commiutative monoids, respectively. Both constructions arise as generalisations of C. Coquand’s data type of fresh lists, and we show how many other free structures also can be realised by other instantiations. Most of our development has been formalised in Agda.
Tue 28 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00
|A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Listsbest paper
|Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
|Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq