TY - GEN
T1 - Logical bisimulations and functional languages
AU - Sangiorgi, Davide
AU - Kobayashi, Naoki
AU - Sumii, Eijiro
PY - 2007
Y1 - 2007
N2 - Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation proof method with "up-to context" techniques. We present logical bisimulations, a form of bisimulation for higherorder languages, in which the bisimulation clause is somehow reminiscent of logical relations. We consider purely functional languages, in particular untyped call-by-name and call-by-value lambda-calculi, and, in each case: we present the basic properties of logical bisimilarity, including congruence; we show that it coincides with contextual equivalence; we develop some up-to techniques, including up-to context, as examples of possible enhancements of the associated bisimulation method.
AB - Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation proof method with "up-to context" techniques. We present logical bisimulations, a form of bisimulation for higherorder languages, in which the bisimulation clause is somehow reminiscent of logical relations. We consider purely functional languages, in particular untyped call-by-name and call-by-value lambda-calculi, and, in each case: we present the basic properties of logical bisimilarity, including congruence; we show that it coincides with contextual equivalence; we develop some up-to techniques, including up-to context, as examples of possible enhancements of the associated bisimulation method.
UR - http://www.scopus.com/inward/record.url?scp=38149036433&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38149036433&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-75698-9_24
DO - 10.1007/978-3-540-75698-9_24
M3 - Conference contribution
AN - SCOPUS:38149036433
SN - 9783540756972
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 364
EP - 379
BT - International Symposium on Fundamentals of Software Engineering - International Symposium, FSEN 2007, Proceedings
PB - Springer Verlag
T2 - 2nd IPM International Symposium on Fundamentals of Software Engineering, FSEN 2007
Y2 - 17 April 2007 through 19 April 2007
ER -