typed lambda calculus

• Ferruccio Guidi. Towards the Unification of Terms, Types and Contexts (typed lambda calculus: abbrevations)
  • KEYWORDS: abbreviations, contexts as terms, types as terms, uniformly dependenttypes
  • ABSTRACT:lambda-delta is a typed lambda calculus intended as the firststep towards the verification of the following conjecture: theadoption of a single set of constructions for terms, types, andcontexts (i.e. the ``contexts as types as terms'' paradigm) iscompatible with the presence of a desirable meta-theory. lambda-deltarealizes the ``types as terms'' paradigm in full and features anuniform typing policy for all binders. Therefore this calculus islambda-typed but differs from the Automath-related calculi in that itprovides for an abbreviation construction at the level of terms. Inthe ``propositions as types'' perspective it can encode theimplicative fragment of predicative logic without quantifiers becauseuniformly dependent types are allowed.
• Thorsten Altenkirch and Nicolas Oury. A core language forDependently Typed Programming (typed lambda calculus: dependent types)
  • KEYWORDS:Functional Programming, core language, recursion
  • ABSTRACT: We discuss the design of a core language, whichshould play a similar role for dependently typed programming likeextensions of System F do for conventional functional languages likeHaskell. The core language incorporates mutual dependent recursivedefinitions, type:type, pi and sigma types and finite sets oflabels. We show that standard constructions from Type Theory includinguniverses can be easily encoded in our language. We address someimportant issues: having an equality checker which unfolds recursiononly when needed, avoiding looping when typechecking "sensible"programs; and the simplification of type checking for eliminators likecase by using equational constraints, allowing the flexible use ofcase expressions within dependently typed programming. We discuss someinteresting extensions: lazy datatypes, integrating equality typeswith constraints and reflection.
• Pierre Corbineau. Towards the end of the Streicher K axiom (asan axiom) (typed lambda calculus: Streicher K axiom)
  • KEYWORDS: Type Theory, Streicher K axiom, Equality,Inductive types
  • ABSTRACT: It is a well known result that the Streicher K axiom, which statesthat all proofs of x=x are canonical, is independent of the rules forthe Calculus of Inductive Constructions. This result has several annoyingconsequences for CIC : the heterogeneous equality (a.k.a. John Majorequality) and the homogeneous equality are not equivalent, and theinjectivity of the second projection does not hold for dependentpairs. In this talk, we present a simple extension of the Calculus ofInductive Constructions that makes the K axiom admissible by allowingmore pattern-matching terms to be correctly typed. We show thatconversely the new theory can be simulated by CIC extended with aconstant representing the K axiom equipped with a correspondingreduction rule and hence is consistent.We finally give several examples of the possibilities offered by thenew type system and discuss the adoption of the heterogeneous equalityas the default equality for CIC.
• Stefan Berghofer and Christian Urban. Nominal Inversion Principles (typed lambda calculus: alpha rule)
  • KEYWORDS: Nominal syntax, Inductive definitions
  • ABSTRACT: When reasoning about inductively defined predicates, such as typing judgements or evaluation relations, proofs are often done by case analysis on the last rule in a derivation. This case analysis involves solving equational constraints on the arguments of the inductively defined predicate athand. This is well-understood in case where term constructors areinjective. In case of alpha equivalence classes, which are not injective, thiscase analysis gives rise to annoying variable renamings. In this paper, weshow that more convenient inversion principles can be derived where one doesnot have to deal with explicit variable renamings. An interesting observationis that this fact relies on the inductive rules to satisfy the variableconvention compatibility condition, which was introduced to justify theadmissibility of Barendregt's variable convention in rule inductions.
• Zhaohui Luo. Modelling object-oriented features in intensionaltype theory (typed lambda calculi: object-oriented features)
  • KEYWORDS: intensional type theory, object-orientedprogramming
  • ABSTRACT: Functional interpretations of object-oriented programming have been studied in the literature by means of type systems with powerful but questionable features such as bounded quantification and manifest types, which have unwelcome concequences including serious meta-theoretic difficulties.In this talk, the modelling of OO-features in class-based languages is studied in intensional type theory. In particular, different from other existing approaches, classes are interpreted as types and their instances ("objects") as objects of the corresponding types. This is made possible in an intensional type theory by considering the parameterised family of inductive unit types and coercive subtyping.Based on such an interpretation, it is then possible to consider the verification of programs with object-oriented features in a proof assistant that implements an intensional type theory.
• Aleksy Schubert. A characterisation of solutions for non-structural subtype constraints
  • KEYWORDS:subtypes, constraint solving, entailment
  • ABSTRACT:The subtype entailment problem is a problem to decide if each solution of a given subtype inequalities constraint set can be a solution of a fixed inequality. This problem is a long time pending problem which was tackled using various techniques.In this work, we present a direct characterisation of all thesolutions of non-structural subtype constraint inequalities. We hopethat this characterisation can lead to better understanding of thesubtype entailment problem.

Linear Logic

• Rene David and Delia Kesner. Strong normalisation of MELL proof-nets (linear logic)
  • KEYWORDS:proof-nets, strong normalisation
  • ABSTRACT:We prove strong normalisation for the multiplicative exponential fragment of linear logic (MELL) proof-nets. In contrast to known proofs of the same result, which are based on the combination of weak normalisation and confluence properties, our proof is inspired from the simple arithmetical proof of strong normalisation for the lambda-calculus, where a natural notion of commutation is used.
• Michele Pagani. Between interaction and semantics: visible acyclic nets (linear logic)
  • KEYWORDS:Linear Logic, Denotational semantics, Weaknormalization, Finiteness spaces, Differential nets
  • ABSTRACT:I present a strict correspondence between cut-elimination, acyclicityand finiteness spaces in the framework of differential nets withpromotion (DiffNet for short). DiffNet have been defined by Ehrhard&Regnier asan extension of the multiplicative exponential linear logic,introducing the semantical constructions defined by Ehrhard in hisfiniteness spaces.Consider the orthogonal (P)Degree of a net P with conclusion C as the setof all nets R with a conclusion notC s.t. the cut between C and notCis weak normalizable. Let P be a cut-free net with conclusion C, myresults show that the following conditions are equivalent:1. P is interpreted as a finitary relation in the finiteness spaceassociated with C2. P is visible acyclic (a geometric condition more general than theusual Danos&Regnier's correctness criterion)3. (P)Degree contains all visible acyclic nets with conclusion notCThese equivalences provide a generalization of the ones in the maintheorems of the theory of linear logic proof-nets, namely: Retore''stheorem (1 --> 2), semantic soundness theorem (2 --> 1), weaknormalization theorem (2 --> 3), and Beche't's theorem (3 --> 2).Above all, it discloses a deep unity in DiffNet among normalization,visible acyclicity and finiteness spaces, which was present (even ifnever actually remarked) only in the multiplicative fragment of linearlogic.
• Alexis Saurin. Interactive Proof Search: Toward Ludics Programming. (linear logic)
  • KEYWORDS: Ludics, (Interactive) Proof Search, LogicProgramming, Interactive Types
  • ABSTRACT: Proof theory and Computation are research areas which have very strong relationships: new concepts in logic and proof theory often apply to the theory of programming languages. The use of proofs to model computation led to the modelling of two main programming paradigms which are functional programming and logic programming. While functional programming is based on proof normalization, logic programming is based on proof search.This approach has been very successful in the sense that it allowed to capture many programming primitives logically. Nevertheless, important fragments of real logic programming languages are still hardly understood from the logical point of view and it has been found very difficult to give a logical semantics to control primitives.Girard introduced Ludics, as a new theory to study interaction. In Ludics, everything is built on interaction or in an interactive way.In this talk, we shall explain how and why Ludics could be consideredas a foundation for interactive proof search. We present the SLAM, anabstract machine (extending Faggian's Loci Abstract Machine fornormalization of designs) allowing to interactively constructdesigns. We examplify interactive proof search on several levels ofexamples (IPS in MALL, runs of the SLAM on simples designs and toyprogramming examples). We then discuss the flexibility we obtain andhow it can be used in order to capture control primitive from logicprogramming.
• Mauro Piccolo and Luca Paolini. Processing Programs: thelinear case (linear logic)
  • KEYWORDS:process calculi, linear programming languages, pcf, linear functions
  • ABSTRACT:We study how to express computational processesgenerated by programs of SlPCF , a very simple paradigmaticprogramming language conceived in order to program functions, linearin a semantic way. For this purpose we adapt the Solos calculusintroduced by Laneve, Parrow and Viktor. We show a fully abstractembedding of SlPCF in Solos, using a typed version of barbedcongruence.
• Marco Gaboardi. Towards a Soft logic for PSPACE
  (linear logic)
  • KEYWORDS:linear logic, Implicit Computational Complexity,type assignment system
  • ABSTRACT:In a previous work we have introduced a type assignment system, named STA_B, correct and complete for PSPACE. STA_B is the first type system characterizing this class using the light logics approach. The expressiveness of STA_B depends on the use, both at type and language level, of Booleans constants managed additively. The soundness is obtained by giving a big step abstract machine that performs programs evaluation in polynomial space.Starting from the ideas underlying STA_B, we would here exploit the proofs-as-programs correspondence to design a logic characterizing PSPACE. The logic system obtained by forgetting terms in STA_B is unsatisfactory. Boolean constants in Soft Linear Logic are redundant. Moreover, the STA_B evaluation mechanism does not directly translate in a standard cut elimination procedure.Starting from these considerations we propose a logic system extendingSoft Linear Logic by an additive cut rule. This system is expressiveenough to characterize all the PSPACE functions. The correctness ofthe cut elimination process is assured by the use of closedreduction.
• Michele Basaldella and Claudia Faggian. Ludics with repetitions: Hyland-Ong style exponentials
  • KEYWORDS:Ludics, Linear Logic, Game Semantics, InteractiveTypes
  • ABSTRACT:Ludics is a research program introduced by J.-Y.Girard whose aim is to provide an interactivefoundation of logic.It can be seen as a form of GameSemantics whose approach is completely based on interaction:strategies are untyped (given on a universal arena) and they caninteract with each other (by composing them).An interactive type is a setof strategies which react the same way to a set of tests(which are strategies themselves).The semantical types which are interpretationof logical formulas enjoy a closure property, called internalcompleteness, which is essential to provefull completeness.In this talk, we extend the original setting of Ludics byintroducing the exponentials in order to interpret proofsof polarizedMELL (Multiplicative-Exponentials-Linear-Logic).To this purpose, we considerHyland-Ong strategies, which naturally admit repetitionof moves.Moreover, we show that we need to extend the universeof strategies by introducing non-uniform strategies:non-uniformity isessential to build exponential types interactively.We show that in our setting itis possible to define interactive types, prove internal completeness,and from this full completeness.

Typed Lambda Calculi: Program Extraction

• Alexandre Miquel. Classical program extraction in the calculus of constructions (classical logic)
  • KEYWORDS: program extraction, classical logic, calculus ofconstructions, lambda-calculus, continuations
  • ABSTRACT: In this talk, I will show that Krivine's techniques of classical realizability can be extended to the calculus of constructions with universes (CCw), which makes possible to define an extraction mechanism from classical proofs (with proof-irrelevance and countable axiom of choice) formalized in Coq (in sort Prop).For that, I will recall the basics of classical realizability, and I will show how to extend Krivine's realisability model (initially defined for 2nd order arithmetic) up to CCw, using a structure of Pi-set which is reminiscent from Hyland and Moggi's omega-sets, Streicher's D-sets and Altenkirch lambda-sets.After having presented the basic extraction scheme, I will discusspossible ways to extend it to inductively defined data-types usingoptimized representations of data structures in the target language.
• Luca Chiarabini. Program Development by Proof Transformation.
  (typed lambda calculus: program extraction)
  • KEYWORDS:Pruning, Program Extraction
  • ABSTRACT:"Prune" a constructive proof means drop somecomputational part of the proof in function, for example, ofadditional knowledge on the input data. Christopher Alan Goad (1980)showed that a program extracted from a pruned proof can be moreperforming w.r.t. a program extracted from the same but not prunedproof. We will show an implementation of the "pruning" method in theMINLOG proof assistant, with an application to the "Bin Packing"Problem. At the end, some ideas on how to extend "pruning" will bepresented.
• Silvia Ghilezan, Hugo Herbelin and Alexis Saurin. A Uniform Approach to Call-by-Name and Call-by-Value Delimited Control
  • KEYWORDS:Classical logic, Observational completeness,Delimited control
  • ABSTRACT:We present a comparative study of the call-by-name and call-by-valuevariants of an extension of lambda mu calculus with delimited control,introduced by Ariola, Herbelin and Sabry, covering in particular thequestions of simple typing, operational semantics, andcontinuation-passing-style semantics. Finally, we discuss therelevance of this calculus as a uniform framework for representing fourdifferent calculi of delimited continuations: two CBV calculi (Danvyand Filinski shift/reset; Sabry shift/lazy reset) and two CBN calculi(a CBN variant of Danvy and Filinski shift/reset; de Groote and SaurinLambda mu calculus -- unexpectedly!).

Typed Lambda Calculi: induction, coinduction and recursion

• Jean-Franc,ois Monin. On defining f91 in Coq (typed lambda calculus: prop-bounded recursive functions)
  • KEYWORDS: Coq, general recursion
  • ABSTRACT:We propose a way to define Prop-bounded recursive functions in theCalculus of Inductive Constructions, using only inductive types(i.e. without auxiliary co-inductive types nor Dybjerinduction-recursion). The technique is illustrated on McCarthy f91function.
• Yves Bertot and Ekaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq
  • KEYWORDS:Coq, Coinduction, Productiveness, Guardedness, Accessibility predicates
  • ABSTRACT:In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions.However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates thatwidens the range of terminative recursive functions formalisable in Constructive Type Theory. In this talk, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation ofcoinductive definitions of productive functions in Coq requires notonly the use of ad-hoc predicates, but also a systematic algorithmthat separates the inductive and coinductive parts of functions.
• Marcin Benke. Multiple Recursion in Type Theory and Generic Programming
  • KEYWORDS:type theory, recursion, generic programming
  • ABSTRACT:Many functions (such as e.g. boolean equality) arenaturally defined by simultaneous recursion in two or morearguments. Yet most formulations of Type Theory allow only primitiverecursion in one argument at a time. We dicsuss some ways in whichmultiplerecursion can be justified and explained in context of genericprogramming in Type Theory.

Typed Lambda Calculi: type assignment algorithm

• Dulma Rodriguez. Algorithmic Subtyping for Higher Order BoundedQuantification Revisited (typed lambda calculus: type assignment algorithm)
  • KEYWORDS:subtyping, bounded quantification
  • ABSTRACT:Algorithmic subtyping for the system Fomegasub of higher order bounded polymorphism has been investigated in the past extensively yielding to positive results. The reason for this new revision of the topic is the development ofnew proof techniques in the recent years and the question, whether thecompleteness of algorithmic subtyping for this system can be provedwith these proof techniques, i.e. syntactically, without constructionof models. We provide a revision of the algorithm and prove directly,using lexicographical induction on kinds and derivations, itssoundness, completeness and termination.
• Davide Ancona, Giovanni Lagorio and Elena Zucca. Type inference for Java-like programs by coinductive logic programming (typed lambda calculus: type assignment algorithm)
  • KEYWORDS: class analysis, coinduction, logic programming, object-oriented programming
  • ABSTRACT: Although coinductive logic programming (Co-LP) has proved to have severalapplications, including for instance verification of infinitaryproperties, model checking and bisimilarity proofs,type inference by Co-LP has not been properly investigated yet.In this presentation we show a novel approach to solve the problem of type inference for Java-like programs based onCo-LP and on the following generic scheme: first, the program P tobe analyzed is translated into a corresponding logic program P'and into a goal G; then, the solution of the type inference problemcorresponds to find a most general substitution theta s.t. (G theta)belongs to the greatest model of P', that is, the coinductive model ofP'. Operationally, this corresponds to find a co-SLD derivation of Gin P', according to the operational semantics of co-LP recentlydefined by Simon et al. [ICLP06,ICALP07].A complete example of instantiation of this scheme is considered for a simpleobject-oriented language with nominal subtyping, where type annotationsare optional. In particular, the following two different type inference problems areconsidered: (1) type inference of a complete program, that is,a collection of classes equipped with a main expression; (2) typeinference of a library of classes, where no main expression is provided.In the final part of the talk we try to address some scalabilityissues of the approach, by sketching some possible instantiations ableto deal with more expressive object-oriented languages.

Typed Lambda Calculi: normalization

• Andreas Abel. Normalization by Evaluation for Martin-Lof TypeTheory (typed lambda calculus: normalization)
  • KEYWORDS: Normalization by Evaluation for Martin-Lof Type Theory
  • ABSTRACT:The decidability of equality is proved for Martin-Lof type theory witha universe 'a la Russell and typed beta-eta-equality judgements. Acorollary of this result is that the constructor for dependent functiontypes is injective, a property which is crucial for establishing thecorrectness of the type-checking algorithm. The decision procedure usesnormalization by evaluation, an algorithm which first interprets termsin a domain with untyped semantic elements and then extracts normalforms. The correctness of this algorithm is established using aPER-model and a logical relation between syntax and semantics.
• Christophe Raffalli. PML and strong normalisation
  (typed lambda calculus: normalization)
  • KEYWORDS: strong normalisation, lambda-calculus, types
  • ABSTRACT: The development of the PML proof assistant is progressing:- the language is now stable- one can start to write proof- the theoretical work is also maturingIn this talk, we will concentrate on the last aspect and mainly thestrong normalisation proof for a subset of the language withoutfixpoint. The proof method is quite different from usual ones mainlybecause we use some kind of constraint checking algorithm (as opposedto usual typing rules of constraint solving).
• Jose Espirito Santo, Ralph Matthes and Luis Pinto. Cgps-translations for intuitionsistic higher-order sequent calculi
  (typed lambda calculus: strong normalization)
  • KEYWORDS:cgps translation, strong normalisation, sequentcalculus, higher order logic
  • ABSTRACT:In this talk we consider type theories defined in the sequent calculus format. Specifically, we want to obtain strong normalisation of these theories as corollary to strong normalisation of the corresponding theories in the natural deduction format. The technique used is called continuation-and-garbage passing style translation, a refinement of cps-translation achieving a strict simulation of reduction in the source calculus by reduction in the target calculus. We review the technique in the propositional / simple type setting, and then we extend it to system F^omega and intuitionistic higher-order logic.Joint work with R. Matthes and L. Pinto.

Foundation of constructive mathematics

• Maria Emilia Maietti and Giovanni Sambin. A minimalist two-level foundation for constructive mathematics (foundation of constructive mathematics)
  • KEYWORDS: intuitionistic logic, quotients, type theory
  • ABSTRACT:We present a two-level theory to formalizeconstructive mathematics. One level is givenby an intensional type theory previously introduced andcalled Minimal type theory. The other level is givenby an extensional set theory which is interpretedin the first one by means of a quotient model.This two-level theory has two main features: it is minimalamong the most relevant foundations for constructive mathematics;it fulfils the ``proofs-as-programs'' paradigm thanks to the waythe two levels are linked.
• Aldo Ursini. Algebraic Types (foundation of typed lambda calculus)
  • KEYWORDS:Types, Algebraic terms
  • ABSTRACT:To a philosopher, a type is a 'co-set'; to a logician, a type is a 'formula'; to a computer scientist a type is a data-type.What is then a type to a poor mathematician? The proposal is: a type is a (FOL)term, i.e. an algebraic term. This is not so silly, as far as one can give an algebraic account for the crucial notions:- being an object a of a given type t;- for such an object a, to be in normal form;- for such an object a, what is a procedure of reduction of a to normal form;- provide some (denotational) semantics for types and objects.This can be achieved using (a common generalization of) classical algebraic notions:ideals of rings, normal subgroups, filters in Heyting or Boolean algebras, etc.; and equational logic.Thus we get a "one-dimensional world": objects, types, derivations areall just algebraic terms. Whence, reduction is handled via equationallogic. And at least in lucky cases -namely when there is a "generic"algebra available-, denotational semantics is dealt with justalgebraic terms.
• Anton Setzer. The strength of Martin-Lof Type Theory with the logical framework (typed lambda calculus: foundations)
  • KEYWORDS:Martin-Lof Type Theory, Proof Theory, Unverses, W-type, Mahlo universe
  • ABSTRACT: Our previous investigations into Martin-Lof Type Theory wererestricted to the version without the logical framework.This avoided having to give an interpretation of Set -all what was needed is to state when the judgementA: Set is correct - this was the case essentially whenthe interpretation of A is a partial equivalence relation.We show how to overcome this problem by interpreting Set andother higher types as proper set theoretic classes.We then determine upper bounds for Martin-Lof Type Theorywith one universe and the W-type, and for the same type theorywith one Mahlo universe and the W-type.
• Guillaume Burel. Encoding Pure Types Systems in Superdeduction
  (typed lambda calculus: subsuming PTS into superdeduction)
  • KEYWORDS:first-order logic, deduction modulo, pure type systems, supernatural deduction
  • ABSTRACT:Superdeduction is a formalism closely related todeduction modulowhich permits to enrich a first-order deductive system---such asnatural deduction or sequent calculus---with new inference rulesautomatically computed from the presentation of a theory. We give anatural encoding from every Pure Type System (PTS) into superdeductionby defining an appropriate first-order theory. We prove that thistranslation is correct and conservative, showing a correspondencebetween valid typing judgment in the PTS and provable sequents in thecorresponding superdeductive system. This implies that superdeductioncan be easily used as a logical framework, and leads to a betterunderstanding of the implementation and the automation of proof searchfor PTS, as well as to more cooperation between proof assistants. Thisalso opens new approaches regarding normalization of PTS.
• • KEYWORDS:
  • ABSTRACT:

Implementations

Automated Deduction

Formalization works

Constructive real analysis

Semantics

Linguistic

Invited Talks