Parameterizations and Fixed-Point Operators on Control Categories
Y. Kakutani (Kyoto University, Japan)
M. Hasegawa (Kyoto University, Japan)

The lambda-mu-calculus features both variables and names, together with their binding mechanisms. This means that constructions on open terms are necessarily parameterized in two different ways for both variables and names. Semantically, such a construction must be modeled by a bi-parameterized family of operators. In this paper, we study these bi-parameterized operators on Selinger's categorical models of the lambda-mu-calculus called control categories. The overall development is analogous to that of Lambek's functional completeness of cartesian closed categories via polynomial categories. As a particular and important case, we study parameterizations of uniform fixed-point operators on control categories, and show bijective correspondences between parameterized fixed-point operators and non-parameterized ones under uniformity conditions.

Inductive types in the Calculus of Algebraic Constructions
F. Blanqui (Ecole Polytechnique, Palaiseau, France)

In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), which is the basis of the proof assistant Coq, can be seen as a Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In this paper, we prove that CIC as a whole can be seen as a CAC, and that it can be extended with non-free constructors, pattern-matching on defined symbols, non-strictly positive types and inductive-recursive types.

A universal embedding for the higher order structure of computational effects
J. Power (The University of Edinburgh, United Kingdom)

We give a universal embedding of the semantics for the first order fragment of the computational Lambda-Calculus into a semantics for the whole calculus. In category theoretic terms, which are the terms of the paper, this means we give a universal embedding of every small freyd -category into a closed freyd-category. The universal property characterises the embedding as the free completion of the Freyd-category as a ->-Set-enriched category under conical colimits. This embedding extends the usual Yoneda embedding of a small category with finite products into its free cocompletion, i.e. the usual category theoretic embedding of a model of the first order fragment of the simply typed Lambda-calculus into a model for the whole calculus, and similarly for the linear Lambda-Calculus. It agrees with an embedding previously given in an ad hoc way without a universal property, so it shows the definitiveness of that construction.

Principal Typing in elementary Affine Logic
P. Coppola (Università di Udine, Italy)
S. Ronchi della Rocca (Università di Torino, Italy)

Elementary Affine Logic (EAL) is a variant of the Linear Logic characterizing the computational power of the elementary bounded Turing machines. The EAL Type Inference problem is the problem of automatically assign to terms of Lambda-calculus EAL formulas as types. This problem is proved to be decidable, and an algorithm is showed, building, for every Lambda-term, either a negative answer or a finite set of type schemata, from which all and only its typings can be derived, through suitable operations.

Functional In-place Update with Layered Datatype Sharing
M. Konecny (The University of Edinburgh, United Kingdom)

Hofmann's LFPL is a functional language with constructs which can be interpreted as referring to heap locations. In this view, the language is suitable for expressing and verifying in-place update algorithms. Correctness of this semantics is achieved by a linear typing. We introduce a non-linear typing of first-order LFPL programs which is more permissive than the recent effect-based typing of Aspinall and Hofmann. The system efficiently infers separation assertions as well as destruction and re-use effects for individual layers of recursive-type values. Thus it is suitable for in-place update algorithms with complicated data aliasing.

Nondederministic Light Logics and NP-Time
F. Maurel (Université Denis Diderot, Paris, France)

This paper relates two distinct traditions: the one of complexity classes characterizations through light logics and models of nondeterminism. Light logics provide an implicit characterization of P-Time algorithms through the Curry-Howard isomorphism : every derivation reduces to its normal form in a polynomial time and every polynomial Turing machine can be simulated by a derivation. In this paper, we extend Intuitionistic Light Affine Logic, a logic with full weakening, with a simple rule for nondeterminism and get a completeness result for NP-Time algorithms which is, as far as we know, the first Curry-Howard characterization of NP complexity. We conclude by a reformulation of the P vs. NP conjecture.

On strong normalisation in the intersection type discipline
G. Boudol (INRIA Sophia Antipolis, France)

We give a proof for the strong normalization result in the intersection type discipline, which we obtain by putting together some well-known results and proof techniques. Our proof uses a variant of Klop's extended lambda-calculus, for which it is shown that strong normalization is equivalent to weak normalization. This is proved here by means of a finiteness of developments theorem, obtained following de Vrijer's combinatory technique. Then we use the standard argument, formalized by Levy as "the creation of redexes is decreasing" and implemented in proofs of weak normalization by Turing, and Coppo and Dezani for the intersection type discipline, to show that a typable expression of the extended calculus is normalizing.

Observational equivalence and program extraction in the Coq proof assistant
N. Oury (Unversité de Paris-Sud, Orsay, France)

The Coq proof assistant allows one to specify and certify programs. Then code can be extracted from proofs to different programming languages. The goal of this article is to substitute, at extraction time, some complex and fast data structures to the structures used for specification and proof. This is made under two principal constraints: (1) this substitution must be correct: the optimized data structures in the extracted program must have the same properties as the original ones, (2) on the proof side, the structure must keep a computable nature. If the framework described here is general, we focus on the case of functional arrays. This work leads us to formalize the notion of observational equivalence in the Coq system. We conclude with benchmarks.

Well-Going Programs Can Be Typed
S. Kahrs (University of Kent, Canterbury, United Kingdom)

We show that the well-behaved functions of untyped PCF are already expressible in typed PCF: any equivalence class of the partial logical equivalence generated from the flat natural numbers in the model given by PCF's operational semantics is inhabited by a well-typed term.

Relative definability and models of Unary PCF
A. Bucciarelli (Université Denis Diderot, Paris, France)
B. Leperchey (Université Denis Diderot, Paris, France)
V. Padovani (Université Denis Diderot, Paris, France)

We show that the poset of degrees of relative definability in the Scott model of Unary PCF is non trivial, and that, nevertheless, the hierarchy of order extensional models of the language is reduced to a bottom element (the fully abstract model) and a top one (the Scott model itself)

Derivatives of containers
M. Abbott (University of Nottingham, United Kingdom)
T. Altenkirch (University of Nottingham, United Kingdom)
N. Ghani (University of Nottingham, United Kingdom)
C. McBride (University of Nottingham, United Kingdom)

We are investigating McBride's idea that the type of one-hole contexts are the formal derivative of a functor from a categorical perspective. Exploiting our recent work on containers we are able to characterize derivatives by a universal property and show that the laws of calculus including a rule for initial algebras as presented by McBride hold --- hence the differentiable containers include those generated by polynomials and least fixpoints. Finally, we discuss abstract containers (i.e. quotients of containers) - this includes a container which plays the role of e in calculus by being its own derivative.

A Logical Framework with Dependently Typed Records
T. Coquand (Chalmers Tekniska Högskola, Göteborg, Sweden)
R. Pollack (The University of Edinburgh, United Kingdom)
M. Takeyama

Our long term goal is a system to formally represent complex structured mathematical objects, and proofs and computation on such objects; e.g. a foundational computer algebra system. Our approach is informed by the long development of module systems for functional programming based on dependent record types as signatures. For our logical purposes, however, we want a dependently typed base language. In this paper we propose an extension of Martin-Löf's logical framework with dependently typed records, and present the semantic foundation and the typechecking algorithm of our system. Some of the work is formally checked in Coq. We have also implemented and experimented with several related systems. Our proposal combines a semantic foundation, provably sound typechecking, good expressiveness e.g. subtyping, sharing) and first-class higher-order modules.

A Fully Abstract Bidomain Model of Unary FPC
J. Laird (University of Sussex, Brighton, United Kingdom)

We present a fully abstract and effectively presentable model of unary FPC (a version of FPC with lifting rather than lifted sums) in the category of bidomains and continuous and stable functions. We show that every element of the bidomain model of unary PCF is definable, and then show that this implies full abstraction for the model of unary FPC. We use a translation into this metalanguage to show that the ``canonical'' bidomain model of the lazy lambda-calculus (with seqential convergence testing) is fully abstract

Encoding of the Monster Type into the Halting Problem & Applications
T. Joly (Catholic University, Nijmegen, Netherlands)

The question whether a given functional of a full type structure (FTS for short) is lambda-definable by a closed lambda-term, raised by G. Huet and known as the Definability Problem, was proved to be undecidable by R. Loader in 1993. More precisely, R. Loader proved that the problem is undecidable for every FTS over at least 7 ground elements. On the other hand, the question is easily decidable for the FTS over a single ground element.We solve here the remaining cases and prove that the problem is undecidable whenever there are more than one ground element. The proof is based on a direct encoding of the Halting Problem for register machines into the Definability Problem restricted to the functionals of the Monster type M = (((o->o)->o)->o)->o->o. It follows that this new restriction of the Definability Problem, which is orthogonal to the ones considered so far, is also undecidable. Another consequence of the latter fact, besides the result stated above, is the undecidability of the beta-Pattern Matching Problem, recently established by R. Loader

Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts
L. Pinto (Universidade do Minho, Braga, Portugal)
J. Espirito Santo (Universidade do Minho, Braga, Portugal)

This work presents the system Lambda-Jm, obtained by extending with cuts Schwichtenberg's multiary sequent calculus. We identify a set of permutative conversions on it, prove their termination and confluence and establish the permutability theorem. Moreover, we show that Lambda-Jm may be seen as an extension of the Lambda-calculus with a notion of generalised multiary application, which encompasses generalised eliminations of von Plato and Herbelin's head-cuts

Proof-Nets with cycles and fixpoint semantics
R. Montelatici (Université Denis Diderot, Paris, France)

Starting from Laurent's work on Polarized Linear Logic, we define a new polarized linear deduction system which handles recursion. This is achieved by extending the cut-rule, in such a way that iteration unrolling is induced by cut-elimination. The proof nets counterpart of this extension is obtained by allowing oriented cycles, which had no meaning in traditional logic. We also free proof nets from additional constraints, leading to a correctness criterion as straightforward as possible (since almost all proof structures are correct). Our system also has a natural and simple semantics, expressed in traced models

On a Semantic Definition of Data Independence
R. Lazic (University of Warwick, Coventry, United Kingdom)
D. Nowak (CNRS & ENS, Cachan, France)

A variety of results which enable model checking of important classes of infinite-state systems are based on exploiting the property of data independence. The literature contains a number of definitions of variants of data independence which are by syntactic restri ctions in particular formalisms. More recently, data independence was defined for labelled transition systems using logical relations, enabli ng results about data independent systems to be proved without reference to a particular syntax. In this paper, we show that the semantic definition is sufficiently strong for this purpose. More precisely, it was known that any syntactically data independent symbolic LTS denotes a semantically data independent family of LTSs, but here we show that the conver se also holds.

Max-plus quasi-interpretations
R. Amadio (Université de Provence, Marseille, France)

Quasi-interpretations are a tool to bound the size of the values computed by a first-order functional program (or a term rewriting system) and thus a mean to extract bounds on its computational complexity. We study the synthesis of quasi-interpretations selected in the space of polynomials over the max-plus algebra determined by the non-negative rationals extended with ∞ and equipped with binary operations for the maximum and the addition. We prove that in this case the synthesis problem is NP-hard, and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. The relevance of multi-linear quasi-interpretations is discussed by comparison to certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity.

Termination and Productivity Checking with Continuous Types
A. Abel (University of Munich, Germany)

We analyze the interpretation of inductive and coinductive types as sets of strongly normalizing terms and isolate classes of types with certain continuity properties. Our result enables us to relax some side conditions on the shape of recursive definitions which are accepted by the type-based termination calculus of Barthe, Frade, Giménez, Pinto and Uustalu, thus enlarging its expressivity.

Abstraction Barrier-Observing Relational Parametricity
J. Hannay (The University of Edinburgh, United Kingdom)

A concept of relational parametricity is developed taking into account the encapsulation mechanism inherent in universal types. This is then applied to data types and refinement, naturally giving rise to a notion of simulation relations that compose for data types with higher-order operations, and whose existence coincides with observational equivalence. The ideas are developed syntactically in lambda calculus with a relational logic. The new notion of abstraction barrier-observing (abo) relational parametricity is asserted axiomatically, and a corresponding abo-parametric per-semantics is devised

A sound and complete CPS-translation for lambda-mu-calculus
K. Fujita (Shimane University, Matsue, Japan)

We investigate injectivity of the novel CPS-translation with surjective pairing. It is syntactically proved that the CPS-translation is sound and complete not only for the extensional lambda-calculus but also for the extensional lambda-mu-calculus.