University of Leicester

computer science

photo of Fer-Jan de Vries 		 	 Dr (Universiteit Utrecht)

STAFF — Fer-Jan de Vries   Dr (Universiteit Utrecht)

Lecturer
F32 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







Research

Infinite computations are a main theme of my interests in the theory and semantics of computation, language and logic.

Recent publications

  1. A. Kurz, D. Petrisan, P. Severi and F.J. de Vries.
    Nominal Coalgebraic Data Types with Applications to Lambda Calculus
    52 pages, accepted for publication in LMCS
    http://arxiv.org/abs/1311.1395 and pdf

    Abstract We investigate final coalgebras in nominal sets. This allows us to define types of infinite data with binding for which all constructions automatically respect alpha equivalence. We give applications to the infinitary lambda calculus.

  2. P. Severi and F.J. de Vries.
    Completeness of Conversion between Reactive Programs for Ultrametric Models
    To appear in TLCA 2013.
    pdf

    Abstract In 1970 Friedman proved completeness of beta eta conversion in the simply-typed lambda calculus for the set-theoretical model. Re- cently Krishnaswami and Benton have captured the essence of Hudak’s reactive programs in an extension of simply typed lambda calculus with causal streams and a temporal modality and provided this typed lambda calculus for reactive programs with a sound ultrametric semantics. We show that beta eta conversion in the typed lambda calculus of reac- tive programs is complete for the ultrametric model.

  3. P. Severi and F.J. de Vries.
    The Infinitary Lambda Calculus of the Infinite Eta Bohm Trees
    Accepted for publication in MSCS.

    Abstract In this paper we introduce a strong form of eta reduction called etabang that we use to construct a confluent and normalising infinitary lambda calculus, of which the normal forms correspond to Barendregt’s infinite eta Bohm trees. This new infinitary perspective on the set of infinite eta Bohm trees allows us to prove that the set of infinite eta B ̈hm trees is a model of the lambda calculus. The model is of interest because it has the same local structure as Scott’s D-infinity-models, i.e. two finite lambda terms are equal in the infinite eta B ̈hm model if and only if they have the same interpretation in Scott’s D-infinity-models

  4. P. Severi and F.J. de Vries.
    Pure Type Systems with Corecursion on Streams
    in Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012.
    pdf

    Abstract In this paper, we use types for ensuring that programs involving streams are well-behaved. We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is called Pure Type Systems with Corecursion (CoPTS). The typed lambda calcu- lus for reactive programs defined by Krishnaswami and Benton can be obtained as a CoPTS. CoPTS’s allow us to study a wide range of typed lambda calculi extended with corecursion using only one framework. In particular, we study this extension for the calculus of constructions which is the underlying formal language of Coq. We use the machinery of infinitary rewriting and formalize the idea of well-behaved programs using the concept of infinitary normalization. We study the properties of infinitary weak and strong normalization for CoPTS’s. The set of finite and infinite terms is defined as a metric completion. We shed new light on the meaning of the modal operator by connecting the modality with the depth used to define the metric. This connection is the key to the proofs of infinitary weak and strong normalization

  5. P. Severi and F.J. de Vries.
    Meaningless Sets in Infinitary Combinatory Logic
    in proceedings of RTA 2012, the 23rd International Conference on Rewriting Techniques and Applications. Editor Ashish Tiwari. Nagoya, May 28 -June 2, 2012. Leibniz International Proceedings in Informatics (LIPIcs) volume 15. Pages 288--304.
    pdf

    Abstract In this paper we study meaningless sets in infinitary combinatory logic. So far only a handful of meaningless sets were known. We show that there are uncountably many meaningless sets. As an application to the semantics of finite combinatory logics, we show that there exist uncountably many combinatory algebras that are not a lambda algebra. We also study ways of weakening the axioms of meaningless sets to get, not only sufficient, but also necessary conditions for having confluence and normalisation.

  6. A. Kurz, D. Petrisan, P. Severi and F.J. de Vries.
    An Alpha-Corecursion Principle for the Infinitary Lambda Calculus
    in postproceedings of CMCS 2012: the 11th International Workshop on Coalgebraic Methods in Computer Science. 31 March - 1 April 2012, Tallinn, Estonia. SLNCS volume 7399, pages 130-149, 2012.
    pdf

    Abstract Gabbay and Pitts proved that lambda-terms up to alpha-equivalence constitute an initial algebra for a certain endofunctor on the category of nominal sets. We show that the terms of the infinitary lambda-calculus form the final coalgebra for the same functor. This allows us to give a corecursion principle for alpha-equivalence classes of finite and infinite terms. As an application, we give corecursive definitions of substitution and of infinite normal forms (Bohm, Levy-Longo and Berarducci trees).

  7. P. Severi and F.J. de Vries.
    Weakening the Axiom of Overlap in Infinitary Lambda Calculus
    in proceedings of RTA2011: the 22nd International Conference on Rewriting Techniques and Applications. Editor Manfred Schmidt-Schauß. Novi Sad. May 30 - June 1, 2011. Leibniz International Proceedings in Informatics (LIPIcs) volume 10. Pages 313--328.
    pdf

    Abstract In this paper we present a set of necessary and sufficient conditions on a set of lambda terms to serve as the set of meaningless terms in an infinitary bottom extension of lambda calculus. So far only a set of sufficient conditions was known for choosing a suitable set of meaningless terms to make this construction produce confluent extensions. The conditions covered the three main known examples of sets of meaningless terms. However, the much later construction of many more examples of sets of meaningless terms satisfying the sufficient conditions renewed the interest in the necessity question and led us to reconsider the old conditions. The key idea in this paper is an alternative solution for solving the overlap between beta reduction and bottom reduction. This allows us to reformulate the Axiom of Overlap, which now determines together with the other conditions a larger class of sets of meaningless terms. We show that the reformulated conditions are not only sufficient but also necessary for obtaining a confluent and normalizing infinitary lambda beta bottom calculus. As an interesting consequence of the necessity proof we obtain for infinitary lambda calculus with beta and bot reduction that confluence implies normalization.






























| [University Home]|[Faculty of Science]|[MCS Home]|[CS Home]||[University Index A-Z]|[University Search]|[University Help]|

Author: Fer-Jan de Vries   Dr (Universiteit Utrecht) (fdv1 at mcs le ac uk), T: +44 (0) 116 252 3903.
© University of Leicester 16 September, 2000 . Last modified: 19th November 2013, 14:00:04.
CS Web Maintainer. Any opinions expressed on this page are those of the author.