Pitts, Andrew M.
Step-Indexed Biorthogonality: a Tutorial Example
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.
BibTeX - Entry
@InProceedings{pitts:DSP:2010:2806,
author = {Andrew M. Pitts},
title = {Step-Indexed Biorthogonality: a Tutorial Example},
booktitle = {Modelling, Controlling and Reasoning About State},
year = {2010},
editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
number = {10351},
series = {Dagstuhl Seminar Proceedings},
ISSN = {1862-4405},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2806},
annote = {Keywords: Biorthogonality, logical relations, operational semantics, step-indexing}
}
|
Keywords: |
|
Biorthogonality, logical relations, operational semantics, step-indexing |
|
Seminar: |
|
10351 - Modelling, Controlling and Reasoning About State
|
|
Issue date: |
|
2010 |
|
Date of publication: |
|
04.11.2010 |
04.11.2010
