Theorem proving for constructive -calculus
From MaRDI portal
Theorem proving for constructive \(\lambda\)-calculus
Recommendations
- Theorem proving for untyped constructive -calculus: Implementation and application
- Proofs and programs
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- Mechanical procedure for proof construction via closed terms in typed calculus
- scientific article; zbMATH DE number 7106482
Cited in
(17)- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- Constructive proofs of the range property in lambda calculus
- The calculus of constructions as a framework for proof search with set variable instantiation
- M-calculus -- a sequent method for automatic theorem proving
- Finite generation and presentation problems for lambda calculus and combinatory logic
- A self-contained provability calculus for \(\varGamma_0\)
- Theorem proving for untyped constructive -calculus: Implementation and application
- scientific article; zbMATH DE number 2185723 (Why is no real title available?)
- Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey
- TLA + Proofs
- Reducibility Proofs in the λ-Calculus
- Formal SOS-Proofs for the Lambda-Calculus
- scientific article; zbMATH DE number 7106482 (Why is no real title available?)
- Types for Proofs and Programs
- On the proof theory of Coquand's calculus of constructions
- Mechanical procedure for proof construction via closed terms in typed calculus
- On connections and higher-order logic
This page was built for publication: Theorem proving for constructive \(\lambda\)-calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2753786)
