This special issue comprises selected papers which were presented at the workshop on dependently typed programming (DTP 10) in Edinburgh in July 2010 – affiliated with Federated Logic conferences (FLOC 10). Earlier workshops on dependently typed programming took place in Nottingham in 2008 (DTP 2008) and there also has been a Dagstuhl seminar (04381) on this subject in 2004. After DTP 2010, in 2011 a workshop on dependently typed programming (DTP 11) took place in Nijmegen affiliated with Interactive Theorem Proving 2011 (ITP 11). In September 2011 there also was a DTP workshop in Shonan, Japan.

We give an algebraic characterization of the syntax and semantics of a class of untyped functional programming languages.

To this end, we introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature (S, A) we associate a category of ‘models’. We then prove that this category has an initial object, which integrates the terms freely generated by S, and which is equipped with reductions according to the rules given in A. We call this initial object the programming language generated by (S, A). Models of a 2-signature are built from relative monads and modules over such monads. Through the use of monads, the models – and in particular, the initial model – come equipped with a substitution operation that is compatible with reduction in a suitable sense.

The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.

The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalizing mathematics is becoming more common and feasible in practice. However, most mature theorem provers lack a direct treatment of partial and general recursive functions; overcoming this weakness has been the objective of intensive research during the last decades. In this article, we review several techniques that have been proposed in the literature to simplify the formalization of partial and general recursive functions in interactive theorem provers. Moreover, we classify the techniques according to their theoretical basis and their practical use. This uniform presentation of the different techniques facilitates the comparison and highlights their commonalities and differences, as well as their relative advantages and limitations. We focus on theorem provers based on constructive type theory (in particular, Agda and Coq) and higher-order logic (in particular Isabelle/HOL). Other systems and logics are covered to a certain extent, but not exhaustively. In addition to the description of the techniques, we also demonstrate tools which facilitate working with the problematic functions in particular theorem provers.

Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a set U of codes and a decoding function T : U → D which assigns to every code u : U, a value T, u of some type D, e.g. the large type Set of small types or sets. The name induction recursion refers to the build-up of codes in U using inductive clauses, simultaneously with the definition of the function T, by structural recursion on codes.

Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation – in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.

We present an interdisciplinary effort in the field of global environmental change, related to the understanding of the concept of ‘vulnerability’. We have used functional programming to capture the generic aspects of the myriad of definitions of vulnerability, and have used the resulting formalization to learn something new about vulnerability and to write some better software for vulnerability assessment. In the process, we have also found out something about formalization in general, about the advantages and disadvantages of dependent types, and about the role of computing science in the larger intellectual landscape.

In this paper, aimed at dependently typed programmers, we present a novel connection between automated and interactive theorem proving paradigms. The novelty is that the connection offers a better trade-off between usability, efficiency and soundness when compared to existing techniques. This technique allows for a powerful interactive proof framework that facilitates efficient verification of finite domain theorems and guided construction of the proof of infinite domain theorems. Such situations typically occur with industrial verification. As a case study, an embedding of SAT and CTL model checking is presented, both of which have been implemented for the dependently typed proof assistant Agda.

Finally, an example of a real world railway control system is presented, and shown using our proof framework to be safe with respect to an abstract model of trains not colliding or derailing. We demonstrate how to formulate safety directly and show using interactive theorem proving that signalling principles imply safety. Therefore, a proof by an automated theorem prover that the signalling principles hold for a concrete system implies the overall safety. Therefore, instead of the need for domain experts to validate that the signalling principles imply safety they only need to make sure that the safety is formulated correctly. Therefore, some of the validation is replaced by verification using interactive theorem proving.