1 citations · 2 across the 6 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2021
Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS
Lorenzo Gheri, Andrei Popescu
We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this companion paper, we instantiate the general theory to the syntax of…
cs.LO2017
A Formalized General Theory of Syntax with Bindings
Lorenzo Gheri, Andrei Popescu
We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are…