research
∙
09/06/2022
Variable binding and substitution for (nameless) dummies
By abstracting over well-known properties of De Bruijn's representation ...
share
research
∙
05/07/2022
A theorem prover and countermodel constructor for provability logic in HOL Light
We introduce our implementation in HOL Light of a prototype of a general...
research
∙
02/11/2021
A formal proof of modal completeness for provability logic
This work presents a formalized proof of modal completeness for Gödel-Lö...
research
∙
07/09/2020
Universal Algebra in UniMath
We present an ongoing effort to implement Universal Algebra in the UniMa...
research
∙
07/09/2020
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
We present an experimental system strongly inspired by miniKanren, imple...
research
∙
11/14/2019
Reduction Monads and Their Signatures
In this work, we study 'reduction monads', which are essentially the sam...
research
∙
03/04/2019
Bicategories in Univalent Foundations
We develop bicategory theory in univalent foundations. Guided by the not...
research
∙
03/03/2019
Modular specification of monads through higher-order presentations
In their work on second-order equational logic, Fiore and Hur have studi...
research
∙
05/09/2018
