Data types as lattices : retractions, closures and projections
De la notion d'opération à celle d'opérateur ou à la recherche de formalismes intrinsèques
Deciding inclusion of set constants over infinite non-strict data structures
Various static analyses of functional programming languages that permit infinite data structures make use of set constants like Top, Inf, and Bot, denoting all terms, all lists not eventually ending in Nil, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics in the set of all, also infinite, computable trees, where all term constructors are non-strict. This...
Definierbare Funktionen im ...-Kalkül mit Typen.
Denotational aspects of untyped normalization by evaluation
We show that the standard normalization-by-evaluation construction for the simply-typed -calculus has a natural counterpart for the untyped -calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...
Denotational aspects of untyped normalization by evaluation
We show that the standard normalization-by-evaluation construction for the simply-typed λβη-calculus has a natural counterpart for the untyped λβ-calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal...
Domain-free -calculus
Domain-Free λµ-Calculus
We introduce a domain-free λµ-calculus of call-by-value as a short-hand for the second order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc-operators cannot, in general, handle correctly the terms placed on the control operator's left, so that the Curry-style system can fail to prove the subject reduction property. Following the continuation semantics, we also discuss the notion of values in classical system,...