DTP on Saturday, July 10th

09:00‑10:00 Invited Talk
09:00 Matthieu Sozeau (Harvard University)
Elaborations in Type Theory

Dependent Type Theory as implemented into proof assistants and programming languages like Coq and Agda provide a firm and general basis for the formalization of mathematics and computer software. However, the core dependent type theory exposes a rather spartan interface for programming and writing proofs. Over the years a number of higher-level constructs and techniques have been developed to overcome this difficulty without touching the core language. For instance, implicit syntax, tactics and meta-languages like Ltac have been used successfully to make systems more accessible, automatable and scalable.

Our research investigates further elaborations from high-level languages into dependent type theory. We present three such elaborations that facilitate programming with proofs, inductive families and overloaded functions in the Coq proof assistant. We demonstrate their usefulness for defining objects and structuring developments, as well as their crucial help in proofs.

10:30‑12:30 Session 4
10:30 Adam Chlipala (Harvard University)
Generating Pieces of Web Applications with Type-Level Programming
11:00 Larry Diehl
Unit & integration test composition via lemmas
11:30 Sean Wilson (University of Edinburgh)
Supporting Dependently Typed Functional Programming with Proof Automation and Testing

I plan to talk about ways in which dependently typed programming with user- defined types and functions can be made more practical by offering improved proof automation and error feedback support. This will be based around the inductive proof automation and program testing features I have developed for Coq that I have recently finished evaluating.

12:00 Karim Kariso (University of Swansea)
Integrating Agda and Automated Theorem Proving Techniques

(joint work with Anton Setzer) Martin-Löf dependent type theory offers a powerful mechanism to construct mathematical formulae and write functional programs; it is essentially typed lambda calculus with the dependent product and algebraic data types. By the Curry-Howard correspondence, propositions can be represented as types, where an element of the type is a proof of the proposition. Another perspective in type theory is that a type is a specification of a problem, and elements of these types are programs.

In this talk I present an embedding of automated theorem proving (ATP) decision procedures into Martin-Löf dependent type theory. The motivation for embedding ATP decision procedures is two fold. Firstly, theorems can be differentiated into two categories, finite and infinite. Finite (and finitisable) theorems can be proven automatically; in the worst case by a brute force algorithm. This category of theories includes typical industrial verification problems, where one wants to verify whether a finite state machine satisfies some property. Infinite theories (or theories with an infinite component) can not in general be proven the same way; this is because a naive attempt would result in non-termination, i.e. an infinite number of proof obligations. The principle of induction is often used to prove infinite theories, resulting in a small finite number of proof objectives. Some theorems have to be strengthened before an inductive proof is possible, in general strengthening a theorem requires a human, preventing a mechanised proof of infinite theories. Thus, the first motivation of this work is to explore a proof framework where the finite components of a theorem are proved automatically and the infinite components are proven with human guidance. This would result in the composition of interactive and automated theorem proving paradigms.

A second motivation is to use the dependently typed programming language and interactive theorem prover Agda as a platform for the efficient development and verification of critical systems. Our ambition is to have a substantial program which actually executes in Agda and is proven to be correct. In this scenario, concrete finite theories need to proven to show the system satisfies some property, and abstract theories need to be proven that show correctness of the verification techniques. Another example of an infinite theorem in this context would include knowledge from the target domain of the critical system, such that any system satisfying certain abstract safety properties is ``safe''.

Briefly, the embedding of the ATP procedure is achieved by assuming a logic, defining the set of formulae and satisfaction relation with respect to the logic. Then the decision procedure is implemented naively and proved to be correct. As a final step, we replace this naive implementation of the decision procedure with an efficient automated theorem prover.

14:00‑15:00 Session 5
14:00 Cezar Ionescu (Potsdam Institute for Climate Impact Research)
Using dependent types in models of climate change impacts

Models of climate change impacts are usually the result of complicated interdisciplinary interactions: one wants, for example, to assess the costs to the economy of implementing various policies designed to keep the average global temperature under certain levels. Many things can go wrong in such an enterprise, and awarness of this is on the rise in the wake of ``Climategate''. We discuss how a dependently typed programming language such as Agda can help. We focus on two issues. First, DTP languages can improve the modeling effort, by providing a framework for defining concepts such as ``vulnerability'', ``resilience'', or ``adaptive capacity'' in a general way. We show an example of this in the model of vulnerability developed at the Potsdam Institute for Climate Impact Research. Second, we see potential for improvements in the reliability of numerical methods used in the models. Classically, numerical methods come with three separate levels: that of the mathematical description, that of the discretization, and that of the implementation. Not only can errors slink in at any of these levels, but each level is related to the others in relatively complicated ways. In a language in which one can formalize constructive mathematics, one can get away with only one level: the mathematical description and the implementation coincide. While it may take awhile for such an implementation to be efficient, it can still be useful for prototyping and testing purposes. Combining the two aspects thus described in an embedded DSL which could be used by modelers of different disciplines could be killer application for dependent types, and a holy grail for climate impact research.

14:30 Hugo Herbelin (INRIA)
A sequent calculus presentation of the Calculus of Inductive Constructions

(joint work with Jeffrey Sarnat, Vincent Siles) The Calculus of Inductive Constructions (CIC) extends Luo's Extended Calculus of Constructions with inductive and coinductive families whose eliminations are decomposed into a combination of dependent pattern matching and, respectively, guarded fixpoints and guarded cofixpoints. The CIC is generally presented in the framework of (call-by-name) natural deduction. We investigate here a (call-by-name) sequent calculus presentation (also known as spine calculus) of the CIC and observe that representing dependent pattern matching in this framework requires the introduction of an notion of dependent cut. We also investigate the dual representation of fixpoints as recursive evaluation contexts (= spines) and cofixpoints as recursive terms and evaluate how far the guardness condition for fixpoints and the guardness condition for cofixpoints can be made syntactically dual one of the other.

15:30‑17:00 Session 6
15:30 Makoto Hamana (University of Gunma)
Another Initial Algebra Semantics of Inductive Families for Programming

There exist already many semantics of dependent types. To model inductive families, usually slice or presheaf categories are used, where the dependency between types is modelled by indexing. In this talk, I try to present another algebraic semantics for inductive families, where the dependency is modelled more explicitly in models rather than indexing. I will show an interesting phenomenon that the dependency derives a kind of polymorphism. It might provide some principle on the reusability of codes for dependently-typed programming.

16:00 Tarmo Uustalu (Institute of Cybernetics, Tallinn)
Safely navigable datastructures with cycles and sharing

(joint work with Varmo Vene, deriving from a collaboration with Makoto Hamana)

16:30 Ulf Norell (Chalmers University)
Lightweight reflection in Agda

We recently added a simple mechanism for reflection to Agda. I'll show some examples of what it lets you do, and some of the limitations.