By abstracting over well-known properties of De Bruijn's representation ...
We introduce our implementation in HOL Light of a prototype of a general...
This work presents a formalized proof of modal completeness for Gödel-Lö...
We present an ongoing effort to implement Universal Algebra in the UniMa...
We present an experimental system strongly inspired by miniKanren,
imple...
In this work, we study 'reduction monads', which are essentially the sam...
We develop bicategory theory in univalent foundations. Guided by the not...
In their work on second-order equational logic, Fiore and Hur have studi...
We present a device for specifying and reasoning about syntax for dataty...