scientific article; zbMATH DE number 863013
From MaRDI portal
Publication:4871733
Recommendations
Cited in
(20)- The calculus of constructions as a framework for proof search with set variable instantiation
- Autarkic computations in formal proofs
- From cut-free calculi to automated deduction: the case of bounded contraction
- M-calculus -- a sequent method for automatic theorem proving
- scientific article; zbMATH DE number 2185723 (Why is no real title available?)
- scientific article; zbMATH DE number 4019061 (Why is no real title available?)
- Automating Proofs in Category Theory
- Automatic Abstraction for Congruences
- A Complete Proof Synthesis Method for the Cube of Type Systems
- scientific article; zbMATH DE number 978243 (Why is no real title available?)
- Theory of types and decision procedures
- Proof search with set variable instantiation in the calculus of constructions
- A mechanized proof system of the third generation calculus in Coq
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- scientific article; zbMATH DE number 3894495 (Why is no real title available?)
- scientific article; zbMATH DE number 6938205 (Why is no real title available?)
- Proof-term synthesis on dependent-type systems via explicit substitutions
- On the proof theory of Coquand's calculus of constructions
- Developing certified programs in the system Coq the program tactic
- On connections and higher-order logic
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4871733)
