Paper Info
Title
A sequent calculus for type theory
Abstract
Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent Calculi (PTSC) by enriching a sequent calculus due to Herbelin, adapted to proof-search and strongly related to natural deduction. PTSC are equipped with a normalisation procedure, adapted from Herbelin’s and defined by local rewrite rules as in Cut-elimination, using explicit substitutions. It satisfies Subject Reduction and it is confluent. A PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising if and only if the latter is. We show how the conversion rules can be incorporated inside logical rules (as in syntax-directed rules for type checking), so that basic proof-search tactics in type theory are merely the root-first application of our inference rules.
Year
DOI
Venue
2006
10.1007/11874683_29
CSL
Keywords
Field
DocType
pure type systems,type checking,sequent calculus,type theory,pure type sequent calculi,corresponding pts,basic proof-search tactic,subject reduction,explicit substitution,conversion rule,natural deduction,satisfiability,pts,inference rule
Logical equivalence,Discrete mathematics,Natural deduction,Subject reduction,Sequent calculus,Proof theory,Type theory,Sequent,Rule of inference,Mathematics
Conference
Volume
ISSN
ISBN
4207
0302-9743
3-540-45458-6
Citations 
PageRank 
References 
5
0.44
17
Authors
3
Name
Order
Citations
PageRank
Stéphane Lengrand116211.43
Roy Dyckhoff245249.09
james mckinna346443.02