The Structural Theory of Pure Type Systems

Reference. The Structural Theory of Pure Type Systems

Cody Roux, Floris van Doorn · TLCA · 2014 · type-theory · DOI

Cite

Cite as @roux-2014-the (helia, typst) · \cite{roux-2014-the} (LaTeX)

BibTeX

bibtex · 1 line

@inbook{roux-2014-the, title={The Structural Theory of Pure Type Systems}, ISBN={9783319089188}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-319-08918-8_25}, DOI={10.1007/978-3-319-08918-8_25}, booktitle={Rewriting and Typed Lambda Calculi}, publisher={Springer International Publishing}, author={Roux, Cody and van Doorn, Floris}, year={2014}, pages={364–378} }

hayagriva YAML (typst)

yaml · 19 lines

roux-2014-the:
  type: chapter
  title: The Structural Theory of Pure Type Systems
  author:
  - Roux, Cody
  - name: Doorn
    given-name: Floris
    prefix: van
  date: 2014
  page-range: 364-378
  url: http://dx.doi.org/10.1007/978-3-319-08918-8_25
  serial-number:
    doi: 10.1007/978-3-319-08918-8_25
    isbn: '9783319089188'
    issn: 1611-3349
  parent:
    type: book
    title: Rewriting and Typed Lambda Calculi
    publisher: Springer International Publishing

Download: roux-2014-the.bib · roux-2014-the.yml

Cites 18 works (0 here)

External (18)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems (2012)
CoqInE: Translating the calculus of inductive constructions into the lambda pi-calculus modulo (2012)
The Dedukti Reference Manual, version 1.0 (2012)
Realizability and Parametricity in Pure Type Systems (2011)
A Polymorphic Lambda-Calculus with Sized Higher-Order Types (PhD thesis, LMU München) (2006)
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems (2004)
Le Calcul des Constructions implicite: syntaxe et sémantique (PhD thesis, Université Paris 11) (2001)
A generic normalisation proof for pure type systems (1998)
On universes in type theory (1998)
Henk: a typed intermediate language (1997)
A Simplification of Girard’s Paradox (1995)
Lambda Calculi with Types (1992)
Modular proof of strong normalization for the calculus of constructions (1991)
ECC, an extended calculus of constructions (1989)
An analysis of Girard’s paradox (1986)
Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieur (PhD thesis, Université Paris VII) (1972)
An intuitionistic theory of types (Tech. Rep., University of Stockholm) (1972)
The Holide home page