Séminaire, 22 septembre 2016

Programme

10:30 – 12:00

Henning Basold (Radboud University)

Invited talk: Dependent Inductive-Coinductive Types: Category Theoretical and Syntactic Perspectives

Dependent types have been pioneered by Per Martin-Löf as a formal framework to carry out intuitionistic mathematics. The major feature of dependent type theories is that definitions, computations and proofs are given in the same language. Moreover, correctness checking of proofs amounts to type-checking, which is well understood. The latter requires though that the associated reduction relation is strongly normalising on all terms a type can depend on, so to obtain an actual algorithm for type checking.

Most formal type systems with dependent types allow the use of inductive types, among other base types, to carry out actually interesting mathematics. Inductive types have been studied vastly in this context, and we know precisely how to incorporate them into dependent type systems with a strongly normalising reduction relation. On the other hand, in computer science, but also in mathematics, we frequently encounter (possibly) infinite computations that are nevertheless well-defined. The concept that emerged to accommodate infinite computations is that of coinductive types. The really interesting examples arise though from the mix of inductive and coinductive types, which has hardly been investigated in the context of dependent type theories.

In this talk, I will present first a category theoretical perspective on dependent type theories that are solely based on mixed inductive-coinductive types. Such theories allow us to encode intuitionistic logic as inductive or coinductive types. Vice versa, we also show that dependent inductive-coinductive types can be constructed in categories with enough structure just from non-dependent inductive types. We then use this high level perspective to set up a syntactic calculus with inductive-coinductive types. For this calculus we will prove that its associated reduction relation preserves types and is strongly normalising. Finally, if time permits, we might discuss future directions of how to internalise bisimilarity on coinductive types into the calculus, while retaining decidable type checking.

The category theoretical view is based on a paper I presented at FICS 2015, whereas the calculus and its properties are joint work with Herman Geuvers presented at LICS 2016.

14:00 – 15:00

Guilhem Jaber (IRIF, Univ. Paris 7)

Invited talk: SyTeCi: Symbolic, Temporal and Circular reasoning for automatic proofs of contextual equivalence

Circular reasoning for automatic proofs of contextual equivalence Operational Techniques (Kripke Logical Relations and Environmental/Open/Parametric Bisimulations) have matured enough to become now formidable tools to prove contextual equivalence of effectful higher-order programs. However, it is not yet possible to automate such proofs -- the problem being of course in general undecidable.

In this talk, we will see how to take the best of these techniques to design an automatic procedure which is able many non-trivial examples of equivalence, including most of the examples from the literature. The talk will describe the main ingredients of this method:

• Symbolic reduction to evaluate of programs,

• Transition systems of heap invariants, as used with Kripke Logical Relations,

• Temporal logic to abstract over the control flow between the program and its environment,

• Circular proofs to automate the reasoning over recursive functions. Using them, we will see how we can reduce contextual equivalence to the problem of non-reachability in some automatically generated transition systems of invariants.

15:30 – 16:30

Pierre Hyvernat (Université de Savoie Mont Blanc Tomme Diot)

Invited talk: Using the Size-Change Principle for checking totality of recursive definitions

The Size-Change Principle (SCP) is a simple algorithm giving a partial termination test for recursive definitions. It is particularly well suited for functional languages with inductive types where recursive functions are given by pattern matching (Caml / Coq) or equations (Haskell / Agda).

If term constructors are lazy, the SCP also gives (by duality) a partial productivity test for recursive functions involving coinductive types. This is what is used in Agda.

Unfortunately, when inductive and coinductive types are nested, this test is unsound: there are "well typed" and terminating recursive definitions producing terms in empty types. Such definitions make Agda inconsistant.

By using ideas from L. Santocanale about circular proof and parity games, I'll show how the SCP can be used to check "totality" of recursive definitions to make sure the definition denote actual objects in their type.

• slides