Abstract. Infinite multi-bases can have infinite and multiple type declarations for the same variable. They can be used as a proof-technique to manipulate only one common basis along the proof....
Continuity and Discontinuity in Lambda Calculus (2008)
Abstract. This paper studies continuity of the normal form and the context operators as functions in the infinitary lambda calculus. We consider the Scott topology on the cpo of the finite and...
Separability of Infinite Lambda Terms (2008)
Abstract. Infinite lambda calculi extend finite lambda calculus with infinite terms and transfinite reduction. In this paper we extend some classical results of finite lambda calculus to infinite...
Femke Van Raamsdonk, Paula Severi, Morten Heine, B. So, Hongwei Xi
This paper surveys a part of the theory of;-reduction in *-calculus which might aptly be called perpetual reductions. The theory is concerned with perpetual reduction strategies, i.e., reduction...
Mariangiola Dezani-ciancaglini, Paula Severi
Universidad de la Rep'ublica Oriental del Uruguay,
Alpha Conversion in Simply Typed Lambda Calculus (2007)
Ana Bove, Paula Severi, Centro De Matematica, Fac De Ciencias
In the usual presentations of simply typed -calculus, it is usual to identify -convertible terms. However, this is not at all a practise in most (typed) functional languages, for which simply typed...
Femke Van Raamsdonk, Paula Severi
Using a characterisation of strongly normalising -terms, we give new and simple proofs of the following: 1. all developments and superdevelopments are finite, 2. a certain rewrite strategy is...
Alpha Conversion in Simply Typed Lambda Calculus (2007)
In the usual presentations of simply typed -calculus, it is usual to identify terms that are ff-convertible. However, this is not at all a practise in most (typed) functional languages, for which...
Alpha Conversion in Simply Typed Lambda Calculus (2007)
In the usual presentations of simply typed -calculus, it is usual to identify terms that are ff-convertible. However, this is not at all a practise in most (typed) functional languages, for which...
appeared in Logical Foundations of Computing Science (LFCS'94), (2007)
Abstract. In this paper, an extension of Pure Type Systems (PTS's) with definitions is presented. We prove this extension preserves many of the properties of PTS's. The main result is a...
Infinite rewriting: from syntax to semantics (2005)
Richard Kennaway, Paula Severi, Ronan Sleep
Rewriting is the repeated transformation of a structured object according to a set of rules. This simple concept has turned out to have a rich variety of elaborations, giving rise to many different...
Internal Program Extraction in the Calculus of Inductive Constructions (2002)
Abstract. Based on the Calculus of Constructions extended with inductive definitions we present a Theory of Specifications with rules for simultaneously constructing programs and their correctness...
A lambda calculus for D∞ (2002)
We define an extension of lambda calculus which is fully abstract for Scott's D_infinity-models. We do so by constructing an infinitary lambda calculus which not only has the confluence...
Böhm's Theorem for Berarducci Trees (2000)
Mariangiola Dezani-ciancaglini, Paula Severi
We propose an extension of lambda calculus which internally discriminates two lambda terms if and only if they have dierent Berarducci trees. 1 Introduction The Lambda Calculus is a theory of...
Böhm's Theorem for Berarducci Trees (2000)
Mariangiola Dezani-Ciancaglini, Paula Severi, Abstractccomputersciencedivision Electrotechnicallaboratory, Thelambdacalculusisatheoryoffunctionsthatservesasafoundationfor Introduction
We propose an extension of lambda calculus which internally discriminates two lambda terms if and only if they have different Berarducci trees.
Perpetual Reductions in λ-Calculus (1999)
Femke Van Raamsdonk, Paula Severi, B. Srensen, Hongwei Xi
This paper surveys a part of the theory of fi-reduction in -calculus which might aptly be called perpetual reductions. The theory is concerned with perpetual reduction strategies, i.e., reduction...
Type Theory and Functional Programming: a work proposal (1997)
Gustavo Betarte, Ana Bove, Juan José Cabezas, Guillermo Calderón, Cristina Cornes, Sylvia Da Rosa, ...
We propose a series of work areas related to program verification, type theory and functional programming. The areas presented are: the implementation of an environment for carrying out constructions...
Normalisation in Lambda Calculus and its relation to Type Inference (1996)
This is an informal explanation of the main concepts and results of [Sev96] 1 . We consider typed and untyped lambda calculi. For untyped lambda calculus, we give a new method to prove properties on...
F. Van Raamsdonk, P. Severi, Issn -x, Femke Van Raamsdonk, Paula Severi
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Pure Type Systems without the Π-condition (1995)
In this paper we define the notion of pure type systems without the \Pi-condition. The \Pi-condition is the requirement that the type of an abstraction is typable. A pure type system without the...
Pure Type Systems with Definitions (1993)
In this paper, an extension of Pure Type Systems (PTS's ) to include definitions is presented and the meta-theory of these PTS's with definitions is treated in detail. We prove that all the...