Proof-search in type-theoretic languages: An introduction

DOI10.1016/S0304-3975(99)00169-3MaRDI QIDQ1575935zbMATH OpenFDO

Authors Didier Galmiche, David Pym

Publication date 23 August 2000

Published in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

logical frameworksproof-objectsproof-searchtype-theoretic languages

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Proof-search in type-theoretic languages
• A focused sequent calculus framework for proof search in pure type systems
• A coinductive approach to proof search through typed lambda-calculi
• scientific article; zbMATH DE number 1348467
• La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
• Workshop on Proof search in type-theoretic languages (in conjunction with CADE-15 conference), Lindau, Germany, July 5, 1998
• Investigations into proof-search in a system of first-order dependent function types
• Type-theoretic languages: Proof search and semantics in conjunction with CADE-17, CMU Pittsburgh, PA, USA, June 20--21, 2000
• Type theory and proof processing systems
• Proof theory of constructive systems: inductive types and univalence

Cites work

• scientific article; zbMATH DE number 3860434 (Why is no real title available?)
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• scientific article; zbMATH DE number 4164201 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• scientific article; zbMATH DE number 1183881 (Why is no real title available?)
• scientific article; zbMATH DE number 3664336 (Why is no real title available?)
• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 15881 (Why is no real title available?)
• scientific article; zbMATH DE number 48279 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 65536 (Why is no real title available?)
• scientific article; zbMATH DE number 108434 (Why is no real title available?)
• scientific article; zbMATH DE number 177784 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 3557754 (Why is no real title available?)
• scientific article; zbMATH DE number 3605078 (Why is no real title available?)
• scientific article; zbMATH DE number 1222428 (Why is no real title available?)
• scientific article; zbMATH DE number 1231511 (Why is no real title available?)
• scientific article; zbMATH DE number 1231530 (Why is no real title available?)
• scientific article; zbMATH DE number 1231698 (Why is no real title available?)
• scientific article; zbMATH DE number 1231699 (Why is no real title available?)
• scientific article; zbMATH DE number 1231701 (Why is no real title available?)
• scientific article; zbMATH DE number 1231702 (Why is no real title available?)
• scientific article; zbMATH DE number 1292293 (Why is no real title available?)
• scientific article; zbMATH DE number 1324433 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 1337625 (Why is no real title available?)
• scientific article; zbMATH DE number 1348471 (Why is no real title available?)
• scientific article; zbMATH DE number 1348473 (Why is no real title available?)
• scientific article; zbMATH DE number 517012 (Why is no real title available?)
• scientific article; zbMATH DE number 517083 (Why is no real title available?)
• scientific article; zbMATH DE number 515728 (Why is no real title available?)
• scientific article; zbMATH DE number 559219 (Why is no real title available?)
• scientific article; zbMATH DE number 599028 (Why is no real title available?)
• scientific article; zbMATH DE number 1113859 (Why is no real title available?)
• scientific article; zbMATH DE number 1158760 (Why is no real title available?)
• scientific article; zbMATH DE number 1489627 (Why is no real title available?)
• scientific article; zbMATH DE number 1499088 (Why is no real title available?)
• scientific article; zbMATH DE number 194511 (Why is no real title available?)
• scientific article; zbMATH DE number 4120168 (Why is no real title available?)
• scientific article; zbMATH DE number 786485 (Why is no real title available?)
• scientific article; zbMATH DE number 786491 (Why is no real title available?)
• scientific article; zbMATH DE number 895271 (Why is no real title available?)
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• scientific article; zbMATH DE number 1406811 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• A Complete Proof Synthesis Method for the Cube of Type Systems
• A Machine-Oriented Logic Based on the Resolution Principle
• A Proof-theoretic Analysis of Goal-directed Provability
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• A framework for defining logics
• A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
• A linear logical framework
• A logical analysis of modules in logic programming
• A relevant analysis of natural deduction
• A resolution theorem prover for intuitionistic logic
• A specification logic for concurrent object-oriented programming
• A unification algorithm for typed -calculus
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Completeness results for linear logic on Petri nets
• Connection-based proof construction in linear logic
• Contraction-free sequent calculi for intuitionistic logic
• Edinburgh LCF. A mechanized logic of computation
• Encoding modal logics in logical frameworks
• Forum: A multiple-conclusion specification logic
• From Petri nets to linear logic
• Games and full completeness for multiplicative linear logic
• Generalized algebraic theories and contextual categories
• Generating plans in linear logic. I: Actions as proofs
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Higher-order unification with dependent function types
• Isabelle. A generic theorem prover
• Kripke Resource Models of a Dependently-typed, Bunched  -calculus
• Kripke-style models for typed lambda calculus
• Labelled proof systems for intuitionistic provability
• Linear Logic Proof Games and Optimization
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Logic and Computation
• Logic programming in a fragment of intuitionistic linear logic
• On Matrices with Connections
• On closed categories of functors
• On connections and higher-order logic
• On proof normalization in linear logic
• On the intuitionistic force of classical search
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Productive use of failure in inductive proof
• Program development in constructive type theory
• Proof strategies in linear logic
• Proof-search in intuitionistic logic based on constraint satisfaction
• Proof-terms for classical and intuitionistic resolution
• Quantales and (noncommutative) linear logic
• Recursive programming with proofs
• Representing proof transformations for program optimization
• Resolution calculus for the first order linear logic
• Resource-distribution via Boolean constraints (extended abstract)
• Simple consequence relations
• Some Properties of Linear Logic Proved by Semantic Methods
• Structured theory presentations and logic representations
• TPS: A theorem-proving system for classical type theory
• The Logic of Bunched Implications
• The OYSTER-CLAM system
• The calculus of constructions
• The foundation of a generic theorem prover
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The system \({\mathcal F}\) of variable types, fifteen years later
• Theorem Proving via General Matings
• Uniform proofs as a foundation for logic programming
• Untersuchungen über das logische Schliessen. I
• Using typed lambda calculus to implement formal systems on a machine

Cited in

(7)

• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• Automata theoretic account of proof search
• Search algorithms in type theory
• Proof Search and Counter Model of Positive Minimal Predicate Logic
• Practical Proof Search for Coq by Type Inhabitation
• Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
• scientific article; zbMATH DE number 1696613 (Why is no real title available?)

Describes a project that uses

Uses Software

• Lolli
• Jape
• Cambridge LCF
• SKIL
• Elf
• XBarnacle
• LEGO
• Automath
• Nuprl
• HOL
• PVS
• TPS
• Isabelle

This page was built for publication: Proof-search in type-theoretic languages: An introduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1575935)