progress on my updates to section 2
This commit is contained in:
Jeremy Siek
parent
ae503a2534
commit
444fd1d3d6
2 changed files with 135 additions and 2 deletions
|
|
@ -283,4 +283,94 @@
|
|||
pages={38--94},
|
||||
year={1994},
|
||||
publisher={San Diego: Academic Press, c1987-}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@article{Abadi-1991,
|
||||
Author = {Abadi, M. and Cardelli, L. and Curien, P.-L. and Levy, J.-J.},
|
||||
Journal = {Journal of Functional Programming},
|
||||
Number = {4},
|
||||
Pages = {375-416},
|
||||
Title = {Explicit Substitutions},
|
||||
Volume = {1},
|
||||
Year = {1991}}
|
||||
|
||||
|
||||
@book{Barendregt-1984,
|
||||
Author = {H.P. Barendregt},
|
||||
Publisher = {Elsevier},
|
||||
Series = {Studies in Logic},
|
||||
Title = {The Lambda Calculus},
|
||||
Volume = {103},
|
||||
Year = {1984}}
|
||||
|
||||
|
||||
@inproceedings{Schafer-Tebbi-Smolka-2015,
|
||||
Author = {Steven Sch{\"{a}}fer and Tobias Tebbi and Gert Smolka},
|
||||
Booktitle = {Interactive Theorem Proving - 6th International Conference},
|
||||
Month = {August},
|
||||
Pages = {359--374},
|
||||
Publisher = {Springer},
|
||||
Series = {ITP},
|
||||
Title = {Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions},
|
||||
Year = {2015}}
|
||||
|
||||
|
||||
@techreport{Pfenning-1992,
|
||||
Address = {Pittsburgh, PA, USA},
|
||||
Author = {Pfenning, Frank},
|
||||
Institution = {Carnegie Mellon University},
|
||||
Number = {CMU-CS-92-186},
|
||||
Title = {A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework},
|
||||
Year = {1992}}
|
||||
|
||||
|
||||
@article{Siek-2017,
|
||||
Author = {Jeremy G. Siek},
|
||||
Journal = {CoRR},
|
||||
Number = {4},
|
||||
Title = {Revisiting Elementary Denotational Semantics},
|
||||
Volume = {abs/1707.03762},
|
||||
Year = {2017}}
|
||||
|
||||
|
||||
@article{Scott-1976,
|
||||
Author = {Dana Scott},
|
||||
Journal = {SIAM Journal on Computing},
|
||||
Number = {3},
|
||||
Pages = {522-587},
|
||||
Title = {Data Types as Lattices},
|
||||
Volume = {5},
|
||||
Year = {1976}}
|
||||
|
||||
|
||||
@article{Engeler-1981,
|
||||
Author = {Engeler, Erwin},
|
||||
Journal = {algebra universalis},
|
||||
Month = {Dec},
|
||||
Number = {1},
|
||||
Pages = {389--392},
|
||||
Title = {Algebras and combinators},
|
||||
Volume = {13},
|
||||
Year = {1981}}
|
||||
|
||||
|
||||
@article{Plotkin-1993,
|
||||
Author = {Gordon D. Plotkin},
|
||||
Journal = {Theoretical Computer Science},
|
||||
Number = {1},
|
||||
Pages = {351 - 409},
|
||||
Title = {Set-theoretical and other elementary models of the λ-calculus},
|
||||
Volume = {121},
|
||||
Year = {1993}}
|
||||
|
||||
|
||||
@article{Barendregt-1983,
|
||||
Author = {Henk Barendregt and Mario Coppo and Mariangiola Dezani-Ciancaglini},
|
||||
Journal = {Journal of Symbolic Logic},
|
||||
Month = {12},
|
||||
Number = {4},
|
||||
Pages = {931-940},
|
||||
Title = {A filter lambda model and the completeness of type assignment},
|
||||
Volume = {48},
|
||||
Year = {1983}}
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@
|
|||
|
||||
\author[adr1]{Wen Kokke}
|
||||
\ead{wen.kokke@ed.ac.uk}
|
||||
\author[adr2]{Jeremy Siek}
|
||||
\author[adr2]{Jeremy G. Siek}
|
||||
\ead{jsiek@indiana.edu}
|
||||
\author[adr1]{Philip Wadler\corref{cor1}}
|
||||
\ead{wadler@inf.ed.ac.uk}
|
||||
|
|
@ -287,6 +287,49 @@ with full normalisation (including reduction under lambda terms). Emphasis
|
|||
is put on the correspondence between the structure of a term and
|
||||
evidence that it is in normal form.
|
||||
|
||||
\paragraph{Substitution: in the untyped lambda calculus}
|
||||
Delves deeper into the properties of simultaneous substitution,
|
||||
establishing the equations of the $\sigma$ algebra of
|
||||
\citet{Abadi-1991}. These equations enable a straightforward proof of
|
||||
the Substitution Lemma~\citep{Barendregt-1984}, which is needed in the
|
||||
next chapter.
|
||||
|
||||
\paragraph{Confluence: of the untyped lambda calculus}
|
||||
Presents a proof of the Church-Rosser theorem based on the classic
|
||||
idea of parallel reduction due to Tait and Martin-L\"of. The proof in
|
||||
Agda is streamlined by the use of ideas from
|
||||
\citet{Schafer-Tebbi-Smolka-2015} and \citet{Pfenning-1992}.
|
||||
|
||||
\paragraph{Big-step: evaluation for call-by-name}
|
||||
Introduces the notion of big-step evaluation to develop a
|
||||
deterministic call-by-name reduction strategy. The main result of this
|
||||
chapter is a proof that big-step evaluation implies the existence of a
|
||||
reduction sequence that terminates with a lambda abstraction.
|
||||
|
||||
\subsection*{Part III, Denotational Semantics}
|
||||
|
||||
\paragraph{Denotational: semantics of the untyped lambda calculus}
|
||||
The early denotational semantics of the lambda calculus based on graph
|
||||
models~\citep{Scott-1976,Engeler-1981,Plotkin-1993} and filter
|
||||
models~\citep{Barendregt-1983} were particularly simple and elegant.
|
||||
This chapter presents such a semantics in a big-step style that is
|
||||
approachable to readers familiar with operational semantics.
|
||||
|
||||
\paragraph{Compositional: the denotational semantics is compositional}
|
||||
TODO
|
||||
|
||||
\paragraph{Soundness: of reduction with respect to denotational semantics}
|
||||
TODO
|
||||
|
||||
\paragraph{Adequacy: of denotational semantics with respect to reduction}
|
||||
TODO
|
||||
|
||||
|
||||
\paragraph{Contextual Equivalence: is implied by denotational equality}
|
||||
TODO
|
||||
|
||||
|
||||
|
||||
\subsection*{Discussion}
|
||||
|
||||
PLFA and SF differ in several particulars. PLFA begins with a computationally
|
||||
|
|
|
|||
Loading…
Reference in a new issue