Formalization of a λ-calculus with explicit substitutions in Coq

DOI10.1007/3-540-60579-7_10zbMath1530.68063OpenAlexW1856419082MaRDI QIDQ6061881

Unnamed Author

Publication date: 8 December 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-60579-7_10

zbMATH Keywords

proof assistantinductive definitioncritical pairlocal confluenceexplicit substitution

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Church-Rosser theorem for a rewriting system on categorical combinators
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Confluence properties of weak and strong calculi of explicit substitutions
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalization of a λ-calculus with explicit substitutions in Coq