A Sequent Calculus for Type Theory

Stephane Lengrand; Roy Dyckhoff; James McKinna

doi:10.1007/11874683

A Sequent Calculus for Type Theory

Stephane Lengrand, Roy Dyckhoff, James McKinna

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Lecture Notes in Computer Science
Editors	Zoltán Ésik
Publisher	Springer-Verlag
Pages	441--455
Number of pages	15
Volume	4207
ISBN (Print)	978-3-540-45458-8
DOIs	https://doi.org/10.1007/11874683
Publication status	Published - 2006

Keywords

type theory
PTS
sequent calculus
proof-search
strong normalisation
Explicit Substitutions

Access to Document

10.1007/11874683

Cite this

@inproceedings{505654ce09c6487882bd4524cbe66640,

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.",

keywords = "type theory, PTS, sequent calculus, proof-search, strong normalisation, Explicit Substitutions",

author = "Stephane Lengrand and Roy Dyckhoff and James McKinna",

year = "2006",

doi = "10.1007/11874683",

language = "English",

isbn = "978-3-540-45458-8",

volume = "4207",

pages = "441----455",

editor = "Zolt{\'a}n {\'E}sik",

booktitle = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag",

address = "Germany",

}

TY - GEN

T1 - A Sequent Calculus for Type Theory

AU - Lengrand, Stephane

AU - Dyckhoff, Roy

AU - McKinna, James

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

KW - type theory

KW - PTS

KW - sequent calculus

KW - proof-search

KW - strong normalisation

KW - Explicit Substitutions

UR - http://www.springerlink.com/content/5l41k74hk5737q4p/

U2 - 10.1007/11874683

DO - 10.1007/11874683

M3 - Conference contribution

SN - 978-3-540-45458-8

VL - 4207

SP - 441

EP - 455

BT - Lecture Notes in Computer Science

A2 - Ésik, Zoltán

PB - Springer-Verlag

ER -

A Sequent Calculus for Type Theory

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this