ProgLog Meetings in 2007

Past meetings of 2007.

Date Speaker Title Extra
Dec 12 Ulf Norell Structurally recursive descent parsing abstract
Dec 5 Martin Hofmann Difunctional Relations and their application to effect-based program transformation abstract
Dec 4 Anton Setzer Inductive-recursive definitions and partial recursive functions abstract
Nov 21 Nils Anders Danielsson A Formalisation of the Correctness Result From "Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures" abstract
Nov 14 Lars Birkedal A Realizability Model of Hoare Type Theory abstract, slides
Oct 17 Randy Pollack Locally nameless representation and nominal Isabelle abstract
Oct 10 Thierry Coquand and Peter Dybjer
abstract
Oct 3 Patrik Jansson Highlights from IFIP 2.1 meeting abstract
Sep 26 Carsten Schürmann A gentle introduction to Delphin abstract
Sep 19 Fredrik Lindblad Automated Proof Construction based on Narrowing abstract
Sep 14 Neil D. Jones The Semantics of ``Semantic Patches" in Coccinelle abstract, mailto:neil@diku.dk
Sep 13 Ralph Matthes Verification of programs involving nested datatypes in intensional type theory abstract
Aug 28 Venanzio Capretta Common Knowledge as a Coinductive Modality abstract
Jun 27 Nils Anders Danielsson Internal automation and metaprogramming abstract
Jun 20 Alexandre Buisse Formalizing categorical models of type theory inside type theory abstract
Jun 6
nationaldagen
May 30
AIM6
May 23 Mats Jansborg Translating Haskell into Agda abstract
May 16 Ulf Norell The with-construct: pattern matching on intermediate results abstract
May 9
AIM6 planning
May 2
TYPES
Apr 18 Nils Anders Danielsson Verification of a Simple Library for Semi-Formal Verification of the Time Complexity of Purely Functional Data Structures abstract
Apr 4 Peter Dybjer Recent news on normalization by evaluation for type theory abstract, slides
Mar 28
VR-applications
Mar 21 Arnaud Spiwack Towards Homological Algebra in Type Theory - A Glimpse in Dependent Type Programming abstract
Mar 14 Andreas Abel Some syntactical normalization proofs abstract
Mar 7 Thierry Coquand What is a model of type theory? abstract, slides
Feb 28 Makoto Takeyama Agda Core Checker Implementation, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-building abstract
Feb 7 Randy Pollack Some Recent Logical Frameworks slides
Jan 31 Nils Anders Danielsson A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family abstract
Jan 24 Ulf Norell A Module System for Agda, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-building abstract, slides


Abstracts of talks in 2007


Structurally recursive descent parsing

Date: Dec 12
Speaker: Ulf Norell
Abstract:
Parser combinators provide a high-level approach to parsing, and we would like to make use of this method in Agda. However, when using parser combinators the cyclic nature of many grammars is reflected as cyclic code, which is rejected by Agda and other languages which require code to be structurally recursive. Furthermore the use of left recursive grammars leads to non-termination with many implementations of parser combinators.

We get around these problems by using a more explicit representation of grammars and by using the type system to statically disallow left recursion. This is done in such a way that most of the flavour of ordinary parser combinators is retained. For instance, users can still define parameterised parsers. Furthermore the type indices used to rule out left recursion can in many cases be inferred automatically by Agda.


Difunctional Relations and their application to effect-based program transformation

Date: Dec 5
Speaker: Martin Hofmann (Ludwig Maximilians Universität, Munich)
Abstract:
In the course of our (with Nick Benton, Lennart Beringer, Andrew Kennedy) investigations of effect-based program transformations we came across the concept of "difunctional relation" (known from the 40s). These are binary relations R such that xRy, zRy, zRw imply xRw.

The talk is about some general properties of those relations and their application in our project.


Inductive-recursive definitions and partial recursive functions

Date: Dec 4
Speaker: Anton Setzer
Abstract:
Inductive-recursive definitions extend the notion of inductive definitions by allowing to define a set inductively while simultaneously defining an element of another type recursively. The type of the constructors for the inductively defined set might depend on the recursively defined function, therefore we cannot separate the recursively defined function from the inductive definition.

Following an approach by Bove and Capretta, we show how to represent partial-recursive functions as inductive-recursive definitions. Then we develop a data type of partial recursive definitions based on the above mentioned closed formalisation. However the resulting data type will be a (large) type. We will show how to compute the functions represented in this data type inside type theory, and obtain a normal form theorem. This theorem allows us to replace this large type by a (small) set.

Finally we discuss the provability and unprovability of recursion theorems.


A Formalisation of the Correctness Result From "Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures"

Date: Nov 21
Speaker: Nils Anders Danielsson
Abstract:
Previously I have talked about a library for semi-formal verification of amortised time bounds for purely functional data structures. This time I will explain how I have formalised the library's correctness statement and proof using Agda.
This presentation provides an example of how one can define a programming language's syntax, type system and semantics as inductive families in a language like Agda. Furthermore it indicates how properties of the language can be proved by induction over these inductive families.


A Realizability Model of Hoare Type Theory

Date: Nov 14
Speaker: Lars Birkedal (IT University of Copenhagen)
Links: slides
Abstract:
We present a denotational model of impredicative Hoare Type Theory, a very expressive dependent type theory in which one can specify and reason about mutable abstract data types. The model ensures soundness of the extension of Hoare Type Theory with impredicative polymorphism; makes the connections to separation logic clear, and provides a basis for investigation of further sound extensions of the theory, in particular equations between computations and types.

Joint work with Rasmus L. Petersen, Aleks Nanevski, Greg Morrisett.


Locally nameless representation and nominal Isabelle

Date: Oct 17
Speaker: Randy Pollack (School of Informatics, Edinburgh University)
Abstract:
The idea that bound variables and free (global) variables should be represented by distinct syntactic classes of names goes back at least to Gentzen and Prawitz. In the early 1990's, McKinna and Pollack formalized a large amount of the metatheory of Pure Type Systems with a representation using two classes of names. This work developed a style for formalizing reasoning about binding which was heavy, but worked reliably. However, the use of names for bound variables is not a perfect fit to the intuitive notion of binding, so I suggested (1994) that the McKinna--Pollack approach to reasoning with two species of variables also works well with a representation that uses names for global variables, and de Bruijn indices for bound variables. This \emph{locally nameless} representation, in which alpha equivalence classes have exactly one element, had previously been used in Huet's Constructive Engine and by Andy Gordon. The locally nameless representation with McKinna--Pollack style reasoning has recently been used by several researchers (with several proof tools) for solutions to the POPLmark Challenge.
In this talk I discuss the current state of play with locally nameless representation and suitable styles of reasoning about it. Using Urban's nominal Isabelle package, it is possible to get the boilerplate definitions and lemmas about freshness of names and swapping/permuting names for free. From nominal Isabelle and other work there are new appraches to proving the strengthened induction principles that reasoning with names requires. There are also some downsides to the new ideas, which I will point out. Among my examples is an isomorphism (proved in nominal Isabelle) between nominal representation and locally nameless representation of lambda terms.


Date: Oct 10
Speaker: Thierry Coquand and Peter Dybjer
Abstract:
Thierry will present shortly a nice example (due to Tobias Nipkow) of proof by reflection: quantifier elimination using functional programming (it may/should be even nicer with dependent types), and Peter will give a report on (one day of) the ICFP meeting.


Highlights from IFIP 2.1 meeting

Date: Oct 3
Speaker: Patrik Jansson
Abstract:
I will present some highlights from the 63rd meeting of IFIP 2.1 on Algorithmic Languages and Calculi. I will pick parts of the following presentations:
Jeuring: Strategic feedback
Oliveira: Generic visitors
Backhouse: Enumerating rationals
Meertens: Specware


A gentle introduction to Delphin

Date: Sep 26
Speaker: Carsten Schürmann (IT University of Copenhagen)
Abstract:
In my talk I will describe and demo the Delphin programming language, which enables programmers to work with dependently typed higher-order encodings. The key technical difficulty that we address is computation over higher-order encodings, which we solve using a variation of Miller and Tiu's nabla-quantifier.


Automated Proof Construction based on Narrowing

Date: Sep 19
Speaker: Fredrik Lindblad
Abstract:
I will report on the progress of implementing a proof search procedure for Agda using narrowing. The idea is to run a narrowing search algorithm on a typechecker implemented in a functional language. This approach has some appealing features:
* The representation of the search procedure is compact and possible to read as well as execute as a type checker for the language.
* Correctness issues are easy to trace since the same code is shared between type checking and type inhabitation.
But simply taking a type checker and applying narrowing does not result in a usable proof construction algorithm. Efficiency must be increased by introducing small modifications and annotations in the code. I will present the most important of them, e.g. parallel conjunction and instantation prioritization. I will also show some examples to give you a flavour of what the parameters of the search are and how far it reaches.


The Semantics of ``Semantic Patches" in Coccinelle

Date: Sep 14
Speaker: Neil D. Jones (DIKU, University of Copenhagen (professor emeritus))
Links: mailto:neil@diku.dk
Abstract:
The Coccinelle system is being developed at DIKU by a research group led by Julia Lawall. It is practically oriented, used for automating and documenting collateral evolutions in Linux device drivers.
In this work we rationally reconstruct the core of the Coccinelle system. A denotational semantics of the system's underlying ``semantic patch language'' (SmPL) is developed, and extended to include variables. The semantics is in essence a higher-order functional program and so executable; but is inefficient and limited to transformation of straight-line source programs.
A richer and more efficient version of SmPL is then defined, and implemented by compiling to the temporal logic CTL-V (CTL with existentially quantified variables ranging over source code parameters and program points; defined using the staging concept from partial evaluation). The compilation is proven correct and a model check algorithm is outlined.


Verification of programs involving nested datatypes in intensional type theory

Date: Sep 13
Speaker: Ralph Matthes (CNRS, Toulouse)
Abstract:
Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Using this flexibility, certain invariants can be maintained in a type system without a need for dependent types.

Verification of programs that exploit nested datatypes has the additional difficulty that statements have to be presented that speak about all the family members in parallel.

A recent extension of the Coq theorem prover provides induction principles for nested datatypes even for type theory with a predicative notion of sets. As a case study, we have proven correct an implementation of redecoration for triangular matrices through a dedicated nested datatype.

For the more complicated case of "truly nested datatypes", there is not yet any direct support by theorem provers. However, by some generalisation of the datatype constructors, we were able to find an induction principle (a mild form of induction-recursion) that could be justified in Coq as well, this time using proof irrelevance and an impredicative universe of sets. Explicit flattening in untyped lambda-calculus is a new case study with this approach.


Common Knowledge as a Coinductive Modality

Date: Aug 28
Speaker: Venanzio Capretta
Abstract:
This is an ongoing attempt to formalize some results in game theory in Coq. We consider a group of agents playing a perfect information game. In general, if the players know nothing about each other, they won't be able to determine an optimal strategy.
But if they have some knowledge about each other strategy, things change. We assume that they are playing rationally, that is, in a way that maximizes their payouts to the best of their knowledge. Besides we assume that they all know that all players are rational, that they know that they all know that they are rational, an so on. This is called "common knowledge" of rationality and can be modeled in Coq by a coinductive predicate. Coinduction can be used to prove some basic principles of epistemic logic.
Under these conditions Aumann's theorem on rationality states that all players will adopt a strategy leading to Backward Induction Equilibrium: a situation in which no player can improve her payoff by changing strategy. The formal proof of Aumann's theorem is the final goal of this project.


Internal automation and metaprogramming

Date: Jun 27
Speaker: Nils Anders Danielsson
Abstract:
I have recently implemented a solver for commutative (semi-) rings in Agda, based on the ideas behind the Coq ring tactic. With this solver equalities like
   (x + y) ^ 3 = x ^ 3 + 3 * x ^ 2 * y + 3 * x * y ^ 2 + y ^ 3
can be proved automatically. Note that the solver is not an external tool; it is implemented in Agda, just like Hedberg's semigroup solver.

I will describe the implementation of the solver, which is rather easy, and how the solver can be used. Using the solver would be easier if Agda had support for metaprogramming, so in the second part of the talk I hope that we can discuss what such a facility could look like, and whether or not we want one.


Formalizing categorical models of type theory inside type theory

Date: Jun 20
Speaker: Alexandre Buisse
Abstract:
We present a formalization of (a categorical model of) type theory in itself, using the notion of categories with families first introduced in Peter's paper "Internal Type Theory". We will present the (still in progress) formalization of this structure in the proof assistant Agda 2, along with the outline of a proof that categories with finite limits are categories with families, which we hope to be significantly easier and more elegant than when using set theory as a metalanguage.


Translating Haskell into Agda

Date: May 23
Speaker: Mats Jansborg
Abstract:
We present the implementation of a method due to Bove and Capretta for translating programs in standard functional programming languages into dependent type theory. To ensure normalisation, we introduce for each function that cannot be proved total, a predicate that characterises its domain. The function is then translated by giving it as an extra argument a proof that the other arguments with which it is called satisfies the predicate. Finally, the function is written by structural recursion on the proof, which guarantees its termination. To avoid rewriting functions unnecessarily, we describe a termination checker based on the size-change method that is used to detect functions that terminate for all inputs, and thus can be translated directly.


The with-construct: pattern matching on intermediate results

Date: May 16
Speaker: Ulf Norell
Abstract:
What the title says.


Verification of a Simple Library for Semi-Formal Verification of the Time Complexity of Purely Functional Data Structures

Date: Apr 18
Speaker: Nils Anders Danielsson
Abstract:
In November I talked about a library for time complexity analysis of purely functional data structures. In this talk I'll discuss the theory underlying the library.

A simple dependently typed lambda calculus with the library functions as primitives will be defined, along with an operational semantics, and I'll sketch a proof showing that the time bounds given by the library are correct. The implementation of the library will also be discussed, as will the close correspondence between the Thunk monad and Capretta's partiality monad.


Recent news on normalization by evaluation for type theory

Date: Apr 4
Speaker: Peter Dybjer
Links: slides
Abstract:
I will give an overview of some ideas on normalization by evaluation for Martin-Löf type theory which Andreas Abel, Thierry Coquand, and I have worked on together recently. I will in particular discuss an algorithm which is closer to Agda's and how it can be explained using normal forms in higher order abstract syntax. I will also give an introduction to categories with families and an algebraic formulation of Martin-Löf type theory, and motivate why our next version of normalization by evaluation will be using this formulation.


Towards Homological Algebra in Type Theory - A Glimpse in Dependent Type Programming

Date: Mar 21
Speaker: Arnaud Spiwack
Abstract:
Kenzo is a tool programmed by Francis Stergereart which computes homology groups of topological states. We present an ongoing work on programming and representing this tool inside type theory. The formalisation of the homology theory is done in the framework of preabelian categories, and raises quite a few questions about dependent types and programming. We discuss the choice of preabelian categories rather than abelian category or set-theoretic point-set algebra and how we make use of the existing features of proof assistants (in this case Coq) to program and prove efficiently with the dependant types.


Some syntactical normalization proofs

Date: Mar 14
Speaker: Andreas Abel
Abstract:
Recently, there has been some interest in lambda-calculi whose normalization can be proven by simple syntactical arguments. For instance, Robin Adams has studied the meta-theory of lambda-free logical frameworks, and Kevin Watkins has designed a logical framework where all terms are in canonical forms. In my talk, I will review some systems with syntactical normalization proofs, like the simply-typed lambda-calculus, predicative polymorphism, and intersection types. I will also discuss how to extend the proof for intersection types by term rewriting, working towards the intersection-type system of the 2006 LICS paper by Thierry Coquand and Arnaud Spiwack.


What is a model of type theory?

Date: Mar 7
Speaker: Thierry Coquand
Links: slides
Abstract:
We recall the presentation of type theory as a generalised algebraic theory, following Cartmell and Peter, and what are the advantages of presenting type theory in this way. Sets provide a model. One would like to represent this model internally in type theory, using sets as types with equivalence relations. One needs then to have an appropriate notion of family of sets, that I will explain. Using this, one can get a type theoretic version of the set theoretic model. Ulf could carry out this formally in agda 2, using the notation facility of agda 2, and I will present also this representation.


Agda Core Checker Implementation, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-building

Date: Feb 28
Speaker: Makoto Takeyama (AIST, Japan)
Abstract:
Bengt and a few others at AIST have been reviewing and reformulating Thierry's Agda core checker program. I will present a set of inference rules alongside the new haskell code (about 250 lines). The issue to discuss is how best to write code as a clear explanation of the core.

Two possible versions in literate haskell are being updated in the COVER cvs.
Agda2/src/core/Makoto/Main.lhs
or
Agda2/src/core/Makoto/CtxCtx.lhs
You need lhs2Tex and foiltex latex class package to latex it.
(lhs2tex -o Main.tex Main.lhs; pdflatex Main.tex)


A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family

Date: Jan 31
Speaker: Nils Anders Danielsson
Abstract:
In this work it is demonstrated how a dependently typed lambda calculus (a logical framework) can be formalised inside a language with inductive-recursive families. The formalisation does not use raw terms; the well-typed terms are defined directly. It is hence impossible to create ill-typed terms.

By proving normalisation, it is shown that the formalisation is usable. Moreover, this proof seems to be the first formal account of normalisation by evaluation for a dependently typed language.

New since last time:
* Explicit substitutions.
* The code is structurally recursive.
* Full normalisation (not just to weak head normal form).
* Equality checker.
* Type checker.


A Module System for Agda, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-building

Date: Jan 24
Speaker: Ulf Norell
Links: slides
Abstract:
When designing the module system for the new version of Agda an important goal has been to make a clear distinction between modules and records. Records are typed first-class entities, whereas modules are simply collections of definitions. An advantage of this approach is that scope checking can be separated from type checking--no type checking is needed to figure out which names a module contains. Although simple, our module system supports a number of useful features: modules inside modules, parameterised modules (similar to sections in Coq), and separate type checking.