Proof-search in type-theoretic languages: An introduction
type: Item
instance of: scholarly article
title: Proof-search in type-theoretic languages: An introduction
zbMATH Open document ID: 0952.03006
DOI: 10.1016/S0304-3975(99)00169-3
published in: Theoretical Computer Science
publication date: 2000-08-23T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 1495210
zbMATH Keywords: proof-objects
zbMATH Keywords: proof-search
zbMATH Keywords: type-theoretic languages
zbMATH Keywords: logical frameworks
author: Didier Galmiche
author: David Pym
describes a project that uses: TPS
describes a project that uses: Automath
describes a project that uses: Elf
describes a project that uses: Cambridge LCF
describes a project that uses: Jape
describes a project that uses: Lolli
describes a project that uses: Nuprl
describes a project that uses: Isabelle
describes a project that uses: PVS
describes a project that uses: HOL
describes a project that uses: LEGO
describes a project that uses: XBarnacle
describes a project that uses: SKIL
MaRDI profile type: Publication
cites work: Games and full completeness for multiplicative linear logic
cites work: Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
cites work: Representing proof transformations for program optimization
cites work: Logic Programming with Focusing Proofs in Linear Logic
cites work: Q3357521
cites work: Theorem Proving via General Matings
cites work: On connections and higher-order logic
cites work: TPS: A theorem-proving system for classical type theory
cites work: Simple consequence relations
cites work: Some Properties of Linear Logic Proved by Semantic Methods
cites work: Using typed lambda calculus to implement formal systems on a machine
cites work: Encoding modal logics in logical frameworks
cites work: Labelled proof systems for intuitionistic provability
cites work: Q4023900
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q4283230
cites work: On Matrices with Connections
cites work: Q4222823
cites work: Q4244301
cites work: Q3327746
cites work: Q3804239
cites work: Q4297316
cites work: Generalized algebraic theories and contextual categories
cites work: A linear logical framework
cites work: Q3867808
cites work: Q4692468
cites work: The calculus of constructions
cites work: Q4289277
cites work: A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
cites work: On closed categories of functors
cites work: A specification logic for concurrent object-oriented programming
cites work: A Complete Proof Synthesis Method for the Cube of Type Systems
cites work: Q4133603
cites work: Contraction-free sequent calculi for intuitionistic logic
cites work: Q4217953
cites work: Higher-order unification with dependent function types
cites work: Completeness results for linear logic on Petri nets
cites work: Q3491030
cites work: Q3743300
cites work: Program development in constructive type theory
cites work: Q4282536
cites work: Q4223030
cites work: Q4223029
cites work: Q4255504
cites work: Q4501142
cites work: On proof normalization in linear logic
cites work: Untersuchungen über das logische Schliessen. I

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3838075

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: The system \({\mathcal F}\) of variable types, fifteen years later

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Linear logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4842966

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4896506

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Edinburgh LCF. A mechanized logic of computation

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A Proof-theoretic Analysis of Goal-directed Provability

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Resource-distribution via Boolean constraints

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A framework for defining logics

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Structured theory presentations and logic representations

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4038661

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Logic programming in a fragment of intuitionistic linear logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4222845

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3999307

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4375633

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Productive use of failure in inductive proof

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Kripke Resource Models of a Dependently-typed, Bunched -calculus

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A relevant analysis of natural deduction

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3862380

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Connection-based proof construction in linear logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3727946

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4842972

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Linear Logic Proof Games and Optimization

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4099613

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3328540

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Generating plans in linear logic. I: Actions as proofs

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: From Petri nets to linear logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A logical analysis of modules in logic programming

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Forum: A multiple-conclusion specification logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Uniform proofs as a foundation for logic programming

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3972527

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Resolution calculus for the first order linear logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Kripke-style models for typed lambda calculus

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4391451

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3999860

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: The Logic of Bunched Implications

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4940727

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4170869

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4264064

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4255509

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Recursive programming with proofs

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4282613

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Logic and Computation

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: The foundation of a generic theorem prover

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Isabelle. A generic theorem prover

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4012879

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4264727

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4883282

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4223032

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q5559220

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A Uniform Proof-theoretic Investigation of Linear Logic Programming

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4012884

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4223033

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: On the intuitionistic force of classical search

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Proof-terms for classical and intuitionistic resolution

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A Machine-Oriented Logic Based on the Resolution Principle

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: An interpretation of Martin-Löf's type theory in a type-free theory of propositions

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Proof strategies in linear logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: A resolution theorem prover for intuitionistic logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4495851

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4733863

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q4264724

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Proof-search in intuitionistic logic based on constraint satisfaction

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Q3999539

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: Quantales and (noncommutative) linear logic

Proof-search in type-theoretic languages: An introduction (cites work)
cites work: The OYSTER-CLAM system

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: Proof-search in type-theoretic languages
Similarity Score: 0.98582387
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
Similarity Score: 0.92971414
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: A coinductive approach to proof search through typed lambda-calculi
Similarity Score: 0.92126
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: Q4264720
Similarity Score: 0.9174343
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
Similarity Score: 0.9145689
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: Workshop on Proof search in type-theoretic languages (in conjunction with CADE-15 conference), Lindau, Germany, July 5, 1998
Similarity Score: 0.91287595
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: Investigations into proof-search in a system of first-order dependent function types
Similarity Score: 0.91182166
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: Type-theoretic languages: Proof search and semantics in conjunction with CADE-17, CMU Pittsburgh, PA, USA, June 20--21, 2000
Similarity Score: 0.90618944
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: Q5438966
Similarity Score: 0.90513176
Recommender Run: Recommender Run 3

Proof-search in type-theoretic languages: An introduction (Recommended article)
Recommended article: Proof Theory of Constructive Systems: Inductive Types and Univalence
Similarity Score: 0.9050936
Recommender Run: Recommender Run 3