More Church-Rosser proofs in \textsc{Beluga}
From MaRDI portal
Publication:6934137
Cites work
- A mechanical proof of the Church-Rosser theorem
- A type theory for defining logics and proofs
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- scientific article; zbMATH DE number 1670493 (Why is no real title available?)
- scientific article; zbMATH DE number 1722714 (Why is no real title available?)
- scientific article; zbMATH DE number 512787 (Why is no real title available?)
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Inductive beluga: programming proofs
- More Church-Rosser proofs (in Isabelle/HOL)
- Operational techniques in PVS -- a preliminary evaluation
- Parallel reductions in \(\lambda\)-calculus
- POPLMark reloaded: mechanizing proofs by logical relations
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Residual theory in λ-calculus: a formal development
- Strongly typed term representations in Coq
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Tree-Manipulating Systems and Church-Rosser Theorems
This page was built for publication: More Church-Rosser proofs in \textsc{Beluga}
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6934137)
