Meta-theory à la carte

DOI10.1145/2429069.2429094zbMath1301.68218OpenAlexW2128448167MaRDI QIDQ2931797

Benjamin Delaware, Tom Schrijvers, Bruno C. d. S. Oliveira

Publication date: 27 November 2014

Published in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2429069.2429094

zbMATH Keywords

Coqextensible Church encodingsmodular mechanized meta-theory

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (5)

Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Ornaments for Proof Reuse in Coq ⋮ Modular Dependent Induction in Coq, Mendler-Style

Uses Software

• Coq
• mini-ML

This page was built for publication: Meta-theory à la carte