Workshop Schedule, October 5, 2007:

 09:00-10:00 Invited Talk (Chair: Hongwei Xi) Jessie: an Intermediate Language for Java and C Verification. Claude Marche. 10:00-10:30 coffee 10:30-12:00 Session I: Monads, Refinement (Chair: Stefan Monnier) Compound Monads in Specification Languages. Jeremy Dawson. A Coinductive Monad for Prop-Bounded Recursion. Adam Megacz. Refined typechecking with Stardust. Joshua Dunfield. 12:00-14:00 lunch 14:00-15:30 Session II: Low-level Types, Dependence (Chair: Martin Sulzmann) The Swiss Coercion. Stefan Monnier. Implementing Reliable Linux Device Drivers in ATS. Rui Shi. Pattern matching coverage checking with dependent types using set approximations. Nicolas Oury. 15:30-16:00 coffee 16:00-17:15 Session III: Equality, Panel (Chair: Aaron Stump) Observational Equality, Now! Thorsten Altenkirch, Conor McBride and Wouter Swierstra. Panel discussion

Abstracts

Some authors have provided PDFs of their papers. The definitive versions of all papers will be in the ACM Digital Library.

Jessie: an Intermediate Language for Java and C Verification. Claude Marche.

Abstract: The Why platform is aimed at proving behavioral properties of both Java and C source code. Both C and Java source are indeed first translated into an intermediate language called Jessie, designed for verification purposes. We present the various features of this language, we show why those features are suitable for verification, and finally how C and Java are translated into it.
Compound Monads in Specification Languages. Jeremy Dawson.

Abstract: We consider the language of extended subsitutions'' involving both angelic and demonic choice. For other related languages expressing program semantics the implicit model of computation is based on a combination of monads by a distributive law. We show how the model of computation underlying extended subsitutions is based on a monad which, while not being a compound monad, has strong similarities to a compound monad based on a distributive law. We discuss these compound monads and monad morphisms between them. We have used the theorem prover Isabelle to formalise and machine-check our results.

Abstract: The coinductive technique of \cite{Capretta2005} is extended with a first-class bind operator, completing the monad and making it possible to directly express higher-order partial functions as well as mutual recursion between functions with different domains.

The inductive invariant technique of \cite{Krstic2003} is extended to allow optional after the fact'' termination proofs. These proofs inhabit members of {\tt Prop}, and therefore do not affect extracted code.

The resulting technique is packaged as a Coq library, and is suitable for formalizing programs written in any side-effect-free functional language with call-by-value semantics.
Refined typechecking with Stardust. Joshua Dunfield. [PDF].

Abstract: We present Stardust, an implementation of a type system for a subset of ML with type refinements, intersection types, and union types, enabling programmers to legibly specify certain classes of program invariants that are verified at compile time. This is the first implementation of unrestricted intersection and union types in a mainstream functional programming setting, as well as the first implementation of a system with both datasort and index refinements. The system---with the assistance of external constraint solvers---supports integer, Boolean and dimensional index refinements; we apply both value refinements (to check red-black tree invariants) and invaluable refinements (to check dimensional consistency). While typechecking with intersection and union types is intrinsically complex, our experience so far suggests that it can be practical in many instances.
Implementing Reliable Linux Device Drivers in ATS. Rui Shi. [PDF].

Abstract: Contemporary software systems often provide mechanisms for extending functionalities, which imposes great safety concerns on the well-being of critical infrastructures. ATS is a recently developed language with its type system rooted in Applied Type System framework which combines linear and dependent type theories for enforcing safe use of resources at low-level. In this paper, we describe a framework for constructing reliable Linux device drivers in ATS. Specifically, drivers are written and type checked in ATS, then compiled and linked to kernel with safety guarantee. Our preliminary experience shows that this approach can effectively enhance the reliability of device drivers and save the testing/debugging time.
The Swiss Coercion. Stefan Monnier. [PDF].

Abstract: Recent type systems allow the programmer to use types that describe more precisely the invariants on which the program relies. But in order to satisfy the type system, it often becomes necessary to help the type checker with extra annotations that justify why a piece of code is indeed well-formed. Such annotations take the form of term-level type manipulations, such as type abstractions, type applications, existential package packing and opening, as well as \emph{coercions}, or \emph{casts}. While those operations have no direct runtime cost, they tend to introduce extra runtime operations equivalent to $\eta$-redexes or even empty loops in order to get to the point where we can apply that supposedly free operation.

We show a coercion that is like a pacific swiss army knife of coercions: it cannot cut but it can instantiate, open, pack, abstract, analyze, or do any combination thereof, reducing the need for extra surrounding runtime operations. And all that, of course, for the price of a single coercion, which still costs absolutely nothing at runtime. This new coercion is derived from Karl Crary's coercion calculus~\cite{Crary00}, but can also replace Crary and Weirich's \kw{vcase}~\cite{Weirich99}.

It additionally happens to come in handy to work around some limitations of value polymorphism. It is presented in the context of Shao et al.'s Type System for Certified Binaries~\cite{Shao02}.

Other than the coercion itself, another contribution of this work is a slightly different proof technique to show soundness of the type erasure.
Observational Equality, Now! Thorsten Altenkirch, Conor McBride and Wouter Swierstra. [PDF].

Abstract: This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type
• which is /substitutive/, allowing us to reason by replacing equal for equal in propositions;
• which reflects the /observable/ behaviour of values rather than their construction (in particular, functions are equal if they take equal inputs to equal outputs);
• which retains /strong/ normalisation, /decidable/ typechecking and /canonicity/---the property that closed normal forms inhabiting datatypes have canonical constructors;
• which allows inductive data structures to be expressed in terms of a standard characterisation of /well-founded trees/;
• which is presented /syntactically/---you can implement it directly, and we are doing so---this approach stands at the core of Epigram 2;
• which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system.
Until now, it has always been necessary to sacrifice some of these aspects.
Pattern matching coverage checking with dependent types using set approximations. Nicolas Oury.

Abstract: Definition of functions by pattern matching has proved to be a key feature of functional programming languages. These definitions allow a clear, easy to read, concise expression of functions. Proof assistants - like the the Coq proof assistant - and some programming languages - like the Epigram or Agda systems - introduce types that can depend on values. These dependent types allow to refine the definition of a type by the use of values. This results in a more precise specification of data types and functions.

For example, it is possible, in such a system, to define the type of the lists of a given length n. The user can then express the fact that the head function - computing the first element of a list - can only be applied to non empty lists. This refinement reduces the number of run times error and allows to integrate program design and program verification.

In presence of dependent types, some cases in a definition by pattern matching can become useless. For example, the case of the empty list is useless in the definition of the function head: the type of this function is specified to prevent the user to apply it to an empty list.

For the sake of clarity and expressivity, we do not want the user to have to handle these useless cases. Especially, if the user is using dependent types for programming, handling such useless cases breaks, by introducing pieces of proof, the natural flow of the program. But forgetting a useful case can break the consistency of the system. This creates the need for a method to safely detect and remove useless cases in a definition by pattern matching.

Alas, this problem - even restricted to algebraic data types - is undecidable in presence of dependent types.

We introduce a new method to detect useless cases based on the computation of over-approximations of the inhabitants of inductive data types and contexts. Not only, this method is proved corrct but can also produce - in a systematic way - a complete matching in Coq, ensuring that the logical power of the system remains unchanged. Moreover, it is modular over the kind of approximated sets used. We give two example implementations of such approximated sets: one is based on truncated terms, the other one on relations linking the number of occurrences of each constructor.