20 citations · 20 across the 4 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2022
Rensets and Renaming-Based Recursion for Syntax with Bindings
Andrei Popescu
I introduce renaming-enriched sets (rensets for short), which are algebraic structures axiomatizing fundamental properties of renaming (also known as variable-for-variable substitu…
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…