Nominal Sets in Agda - A Fresh and Immature Mechanization

DOI10.4204/eptcs.376.7arXiv2303.13252OpenAlexW4353057058MaRDI QIDQ6118749

Miguel Pagano, Unnamed Author

Publication date: 28 February 2024

Published in: Electronic Proceedings in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2303.13252

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cites Work

• A new approach to abstract syntax with variable binding
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
• Nominal Sets
• Formalising the pi-calculus using nominal logic
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Nominal Sets in Agda - A Fresh and Immature Mechanization