Commit ad91dd0a authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents 88e6ce23 5de56add
......@@ -333,4 +333,14 @@ doi = "https://doi.org/10.1016/S0747-7171(89)80045-8",
url = "http://www.sciencedirect.com/science/article/pii/S0747717189800458",
author = "Masako Takahashi",
abstract = "The notion of parallel reduction is extracted from the Tait-Martin-Löf proof of the Church-Rosser theorem (for β-reduction). We define parallel β-, η- and βη-reduction by induction, and use them to give simple proofs of some fundamental theorems in λ-calculus; the normal reduction theorem for β-reduction, that for βη-reduction, the postponement theorem of η-reduction (in βη-reduction), and some others."
}
@book{Bar84,
author = {H. P. Barendregt},
title = {The Lambda Calculus Its Syntax and Semantics},
publisher = {North Holland},
year = {1984},
volume = {103},
edition = {Revised},
note = {http://www.cs.ru.nl/~henk/Personal Webpage}
}
\ No newline at end of file
......@@ -253,7 +253,8 @@ and that, under certain restrictions it is also complete.
\end{lemma}
\begin{proof}
This is a known result for the $\lambda-$calculus (even
extended with conditional, and basic types), see for instance
extended with conditional, and basic types), obtained using
the Tait and Martin-Löf technique (\cite{Bar84}). See for instance
\cite{Taka89} and \cite{Levy2017}.
The additional substitutions made by the rule \Rule{TestCtx}
will be performed later with the standard semantics.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment