A Complete Proof Synthesis Method for the Cube of Type Systems
From MaRDI portal
Publication:4276174
DOI10.1093/logcom/3.3.287zbMath0789.68123OpenAlexW1969881696MaRDI QIDQ4276174
Publication date: 20 June 1994
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/logcom/3.3.287
Related Items
Practical Proof Search for Coq by Type Inhabitation, Hammer for Coq: automation for dependent type theory, Developing certified programs in the system Coq the program tactic, Proof search with set variable instantiation in the Calculus of Constructions, An algorithm for checking incomplete proof objects in type theory with localization and unification, Proof-term synthesis on dependent-type systems via explicit substitutions, Automorphisms of types and their applications, The calculus of constructions as a framework for proof search with set variable instantiation, Proof-search in type-theoretic languages: An introduction, Higher order unification via explicit substitutions
