DTP on Friday, July 9th

09:00‑10:00 Invited Talk
09:00 Ana Bove (Chalmers University)
10 Years of Partiality and General Recursion

Constructive type theory (CTT) [MLTT, CoC], even if originally developed for formalising mathematics, has been seen as a programming language with dependent types for the past 30 years.

CTT is a theory of total functions. This clearly rules out genuine partial function. Most systems based on CTT only allow structurally recursive functions as a way to guarantee totality. These limitations are really a problem when we are faced with the task of formalising and proving correct a function that do not satisfy the requirements.

The search for methodologies to simplify the formalisation of general recursive and partial function in CTT has been a hot topic during the last decade. Many ideas of different nature have been developed in order to facilitate the definition of this class of functions and their subsequent proof of correctness. However, the issue of how to best formalise recursive and partial functions is far from being resolved.

In this talk we will have a look at some of the methodologies that have been popularised in the last few years. We will mainly concentrate on methodologies available for systems like Coq and Agda, but we will also discuss some of the methodologies available for Isabelle/HOL. Though Isabelle/HOL is not based on CTT but on classical high-order logic, functions should be total in Isabelle/HOL if one is to use to system as a theorem prover.

10:30‑12:30 Session 1
10:30 Andreas Abel (University of Munich)
Parametric Dependent Function Types
11:00 Edwin Brady (University of St Andrews)
Practical, efficient programming with dependent types
11:30 Anton Setzer (University of Swansea)
Coalgebras in dependent type theory

We review our desired way of representing weakly final coalgebras in dependent type theory. We illustrate why this representation avoids the confusion arising when using codata types. We determine a model for the resulting theory and show its consistency.

12:00 Nils Anders Danielsson (University of Nottingham)
Operational Semantics Using the Partiality Monad

An operational semantics for a partial language is usually defined as a relation, either in the form of a small-step semantics or as a big-step semantics. I will discuss an alternative approach: by using the partiality monad one can define the semantics as a total function. This makes it possible to state compiler correctness in a way which I find easier to understand (and hence get right). Instead of separate statements dealing with termination, non-termination, crashes, raised exceptions, and so on, one can get by with a single, uniform statement.

14:00‑15:00 Session 2
14:00 Darin Morrison (University of Nottingham)
Mechanizing Metatheory via Dependently Typed Programming
14:30 Antonis Stampoulis (Yale University)
VeriML: Type-safe computation of logical terms inside a language with effects

Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Unfortunately, large scale proof development in these proof assistants is still a difficult and time-consuming task. One major weakness of these proof assistants is the lack of a single language where users can develop complex tactics and decision procedures using a rich programming model and in a typeful manner. This limits the scalability of the proof development process, as users avoid developing domain-specific tactics and decision procedures.

In this talk we will present VeriML, a novel language design that couples a type-safe effectful computational language with first-class support for manipulating logical terms such as propositions and proofs. The main idea behind our design is to integrate a rich logical framework--similar to the one supported by Coq--inside a computational language inspired by ML. The language design is such that the added features are orthogonal to the rest of the computational language, and also does not require significant additions to the logic language, so soundness is guaranteed. We have built a prototype implementation of VeriML including both its type-checker and an interpreter. Examples of type-safe tactics and decision procedures written in VeriML will be given.

15:30‑17:00 Session 3
15:30 Carsten Schuermann (IT University Copenhagen)
The HOL-Nuprl connection in Delphin

(joint work with Adam Poswolsky) Howe's HOL/Nuprl connection is an interesting example of a translation between two fundamentally different logics, namely a typed higher-order logic and a polymorphic extensional type theory. In earlier work we have established a proof-theoretic correctness result of the translation in a way that complements Howe's semantics-based justification and furthermore goes beyond the original HOL/Nuprl connection by providing the foundation for a proof translator. Using the dependently typed language Delphin, this present paper goes one step further: We give a total and executable Delphin program that translates proofs from HOL into Nuprl.

16:00 Brigitte Pientka (McGill University)
Type reconstruction in dependently typed programming

Over the past decade, different flavors of dependent types have slowly found their way into mainstream programming. Yet, many issues around dependent types are still ill-understood.

In this talk, I will concentrate on the issue of type reconstruction for a dependently typed functional language where we separate the dependently typed term language from the dependently typed computation language. We first present a decidable type checking algorithm. Next, we outline a type reconstruction algorithm which when given a source-level program where some type arguments are omitted will return a fully explicit program.

We believe our description provides general insights into how to develop type reconstruction algorithms for dependently typed programming and we have used the described methodology for type reconstruction in Beluga, a programming and reasoning environment for formal systems.

16:30 Dan Licata (Carnegie Mellon University)
Security-Typed Programming within Dependently Typed Programming

(joint work with Jamie Morgenstern)