

@phdthesis{Luo:PHD90,
  author =        {Z. Luo},
  note =          {CST-65-90/ECS-LFCS-90-118},
  school =        {Department of Computer Science, University of
                   Edinburgh},
  title =         {An Extended Calculus of Constructions},
  year =          {1990},
}

@phdthesis{Girard1972,
  author =        {Girard, J. Y},
  school =        {Université de Paris 7},
  type =          {These d'état},
  title =         {Interprétation fonctionnelle et elimination des
                   coupures de l'arithmétique d'ordre supérieur},
  year =          {1972},
}

@article{Tait67,
  author =        {Tait, William},
  journal =       {J. Symb. Log.},
  number =        {2},
  pages =         {198-212},
  title =         {Intensional {I}nterpretations of {F}unctionals of
                   {F}inite {T}ype {I}},
  volume =        {32},
  year =          {1967},
}

@inproceedings{Goguen:TLCA95,
  author =        {Healfdene Goguen},
  booktitle =     {2nd International Conference on Typed Lambda Calculi
                   and Applications (TLCA'95)},
  editor =        {Mariangiola Dezani-Ciancaglini and Gordon Plotkin},
  pages =         {186--200},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science (LNCS 902)},
  title =         {Typed operational semantics},
  year =          {1995},
  abstract =      {This paper introduces typed operational semantics, a
                   class of formal systems which define a reduction to
                   normal form for the welltyped terms of a particular
                   type theory. These systems lead to a new approach to
                   the metatheory for type theories, which we develop
                   here for the simply typed lambda calculus. A similar
                   approach can be used to study systems with dependent
                   types.},
  doi =           {10.1007/BFb0014053},
  isbn =          {978-3-540-49178-1},
  url =           {https://doi.org/10.1007/BFb0014053},
}

@incollection{Crary:ATAPL,
  author =        {Karl Crary},
  booktitle =     {Advanced Topics in Types and Programming Languages},
  editor =        {Bejamin C. Pierce},
  publisher =     {The MIT Press},
  title =         {Logical Relations and a Case Study in Equivalence
                   Checking},
  year =          {2005},
}

@article{Harper03tocl,
  author =        {Robert Harper and Frank Pfenning},
  journal =       {ACM Transactions on Computational Logic},
  number =        {1},
  pages =         {61-101},
  title =         {On Equivalence and Canonical Forms in the {LF} Type
                   Theory},
  volume =        {6},
  year =          {2005},
}

@techreport{Watkins02tr,
  author =        {Kevin Watkins and Iliano Cervesato and Frank Pfenning and
                   David Walker},
  institution =   {Department of Computer Science, Carnegie Mellon
                   University},
  number =        {CMU-CS-02-101},
  title =         {A Concurrent Logical Framework {I}: Judgments and
                   Properties},
  year =          {2002},
}

@techreport{Raamsdonk_onnormalisation,
  author =        {Femke van Raamsdonk and Paula Severi},
  institution =   {Technische Universiteit Eindhoven},
  number =        {95/20},
  title =         {On Normalisation},
  year =          {1995},
}

@article{Joachimski2003,
  author =        {Felix Joachimski and Ralph Matthes},
  journal =       {Archive for Mathematical Logic},
  month =         {Jan},
  number =        {1},
  pages =         {59--87},
  title =         {Short proofs of normalization for the simply- typed
                   $\lambda$-calculus, permutative conversions and
                   {G}{\"o}del's {T}},
  volume =        {42},
  year =          {2003},
  abstract =      {{\enspace}Inductive characterizations of the sets of
                   terms, the subset of strongly normalizing terms and
                   normal forms are studied in order to reprove weak and
                   strong normalization for the simply-typed
                   $\lambda$-calculus and for an extension by sum types
                   with permutative conversions. The analogous treatment
                   of a new system with generalized applications
                   inspired by generalized elimination rules in natural
                   deduction, advocated by von Plato, shows the
                   flexibility of the approach which does not use the
                   strong computability/candidate style {\`a} la Tait
                   and Girard. It is also shown that the extension of
                   the system with permutative conversions by
                   $\eta$-rules is still strongly normalizing, and
                   likewise for an extension of the system of
                   generalized applications by a rule of ``immediate
                   simplification''. By introducing an infinitely
                   branching inductive rule the method even extends to
                   G{\"o}del's T.},
  doi =           {10.1007/s00153-002-0156-9},
  issn =          {1432-0665},
  url =           {https://doi.org/10.1007/s00153-002-0156-9},
}

