 |
STAFF
— Fer-Jan de Vries
Lecturer
|
F32 Mathematics & Computer Science Building
Department of Computer Science,
University of Leicester,
University Road,
Leicester,
LE1 7RH.
T: +44 (0) 116 252 3903
E: fdv1 at mcs le ac uk
|
A selected annotated bibliography
- J.R. Kennaway and F.J. de Vries. Infinitary Rewriting. Chapter
12 in Terese, editor, Term Rewriting Systems (Cambridge Tracts in
Theoretical Computer Science 55), Cambridge University Press. Page
668-711. 2003.
This is a survey paper on our theory of infinitary rewriting. It
provides techniques for completing finitary orthogonal rewriting
systems with infinite terms and infinite reduction while maintaining
the confluence property.
- P. Severi and F.J. de Vries. An Extensional Böhm Model.
Conference paper in Sophie Tison, editor, Rewiting Techniques and
Applications, Proceedings of the 13th International Conference, RTA
2002, Copenhagen Denmark, July 2002. (Lecture Notes in Computer
Science 2378), Springer-Verlag. Page 159-173. 2002.
We show the existence of an infinitary confluent and normalising
extension of the finite extensional lambda calculus with beta and
eta. Two consequences: (i) a simple construction of an extensional
Böhm model of the finite lambda calculus; (ii) a simple, syntax based
proof that two lambda terms are equal in this model if and only if
they have the same eta- Böhm tree if and only if they are
observationally equivalent wrt to beta normal forms.
- S. van Bakel, F. Barbanera, M. Dezani-Ciancaglini, F.J. de Vries.
Intersection Types for Lambda Trees. Theoretical Computer Science
272(1-2): 3-40, 2002.
We introduce a type assignment system which is parametric with
respect to five families of trees obtained by evaluating lambda terms
(eta- Böhm trees, Böhm trees, Lévy-Longo trees, etc). Then we prove,
in an (almost ) uniform way that each type assignment system fully
describes the observational equivalences induced by the corresponding
tree representation of lambda trees.
- M. Dezani-Ciancaglini, P. Severi and F.J. de Vries. Infinitary
Lambda Calculus and Discrimination. Theoretical Computer Science
298(2):275 - 302, 2003.
We propose an extension of lambda calculus for which the
Berarducci trees equality coincides with observational equivalence,
when we observe rootstable or rootactive behavior of terms. In one
direction the proof is an adaptation of the classical Böhm out
technique. In the other direction the proof is based on confluence for
strongly converging reductions in this extension.
-
P. Severi and F.J. de Vries. Continuity and Discontinuity in
Lambda Calculus. Conference paper in Pawel Urzyczyn, editor, Typed
Lambda Calculus and Applications, Proceedings of the 7th International
Conference, TLCA 2005, Nara Japan, April 21-23 2005. (Lecture Notes in
Computer Science 3461), Springer-Verlag. Page 369-385. 2005.
We give concrete descriptions of a number of new syntactic models
of the lambda calculus and we show that in the class of the syntactic
models that can be constructed from a set of undefined terms only the
Böhm model and the Lévy-Longo model are continuous.
- P. Severi and F.J. de Vries. Order Structures on Böhm-like Models.
Conference paper in Luke Ong, editor, Computer Science Logic: 19th
International Workshop, CSL 2005, 14th Annual Conference of the EACSL,
Oxford, UK. August 22-25, 2005. (Lecture Notes in Computer Science
3634), Springer-Verlag. Page 103-116. 2005.
We study orderability of the syntactic lambda
models that can be constructed from a set of undefined terms. Some
models can be ordered by the prefix relation. The Berarducci trees can
be orderded with the new ogre relation. And we show that there are
many models that can not be ordered at all.
|
|