|
[2010]
|
Matthias Mann and
Manfred Schmidt-Schauß.
Similarity implies equivalence in a class of non-deterministic
call-by-need lambda calculi.
Information and Computation, 208(3):276 - 291, 2010.
[ bib |
http ]
|
|
[2008]
|
Manfred Schmidt-Schauß and
Matthias Mann.
On equivalences and standardization in a non-deterministic
call-by-need lambda calculus.
Frank report 31, Institut für Informatik. Fachbereich Informatik
und Mathematik. J. W. Goethe-Universität Frankfurt am Main, September 2008.
[ bib |
PDF |
previous version (2.0) |
previous version (1.0) ]
|
|
[2006]
|
Matthias Mann and
Manfred Schmidt-Schauß.
How to prove similarity a precongruence in non-deterministic
call-by-need lambda calculi.
Frank report 22, Institut für Informatik. Fachbereich Informatik
und Mathematik. J. W. Goethe-Universität Frankfurt am Main, January 2006.
[ bib |
PDF ]
|
|
[2005]
|
Matthias Mann.
A Non-Deterministic Call-by-Need Lambda Calculus: Proving
Similarity a Precongruence by an Extension of Howe's Method to Sharing.
Dissertation, Johann Wolfgang Goethe-Universität, Frankfurt,
2005.
[ bib |
German Abstract |
PDF ]
|
|
[2005]
|
Matthias Mann.
Congruence of bisimulation in a non-deterministic call-by-need lambda
calculus.
Electronic Notes in Theoretical Computer Science,
128(1):81-101, May 4, 2005.
[ bib |
Corrigendum ]
|
|
[2004]
|
Matthias Mann.
Towards Sharing in Lazy Computation Systems.
Frank report 18, Institut für Informatik, J.W. Goethe-Universität
Frankfurt am Main, December 2004.
Available on request.
[ bib ]
|
|
[2004]
|
Matthias Mann.
Congruence of bisimulation in a non-deterministic call-by-need lambda
calculus.
In Luca Aceto, Willem Jan Fokkink, and Irek Ulidowski, editors,
Preliminary Proceedings of the Workshop on Structural Operational Semantics,
SOS '04, (London, United Kingdom, August 30, 2004), volume
NS-04-1 of
BRICS Notes Series,
pages 20-38, August 2004.
Please refer to the
revised PDF.
[ bib |
presentation ]
We present a call-by-need lambda-calculus Lambda-ND with an erratic
non-deterministic operator pick and a non-recursive let. A definition
of a bisimulation is given, which has to be based on a further
calculus named Lambda-Approx, since the naive bisimulation definition
is useless. The main result is that this bisimulation is a congruence
and contained in the contextual equivalence.
The proof is a non-trivial extension of Howe's method. This might be a
step towards in defining useful bisimulation relations and proving
them to be congruences in calculi that extend the Lambda-ND-calculus.
Keywords: Bisimulation, Congruence, Contextual Equivalence, Non-determinism, Call-by-need Lambda Calculus
|
This file has been generated by
bibtex2html 1.69
|
|