DagSemProc.10351.6.pdf
- Filesize: 0.49 MB
- 10 pages
Document
Step-Indexed Biorthogonality: a Tutorial Example
Author
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 10351
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2010-11-04
Cite AsGet BibTex
Andrew M. Pitts. Step-Indexed Biorthogonality: a Tutorial Example. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/DagSemProc.10351.6
https://doi.org/10.4230/DagSemProc.10351.6
Abstract
The purpose of this note is to illustrate the use of step-indexing combined with biorthogonality to construct syntactical logical relations. It walks through the details of a syntactically simple, yet non-trivial example: a proof of the "CIU Theorem'' for contextual equivalence in the untyped call-by-value $lambda$-calculus with recursively defined functions.
Keywords
- Biorthogonality
- logical relations
- operational semantics
- step-indexing
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads