7 citations · 27 across the 17 of their papers we have counts for
18 papers
Variable binding and substitution for (nameless) dummies
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont +1
By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitut…
Mechanising Gödel-Löb provability logic in HOL Light
Marco Maggesi, Cosimo Perini Brogi
We introduce our implementation in HOL Light of the metatheory for Gödel-Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuri…
A formal proof of modal completeness for provability logic
Marco Maggesi, Cosimo Perini Brogi
This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss som…
Universal Algebra in UniMath
Gianluca Amato, Matteo Calosci, Marco Maggesi +1
We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to impl…
Universal Algebra in UniMath
Gianluca Amato, Marco Maggesi, Maurizio Parton +1
We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a pro…
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
Marco Maggesi, Massimo Nocentini
We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mecha…