PLPV on Monday, August 21st

Session 1: Martin-Loef Type Theory (09:00‑10:30)

09:00‑10:00

Peter Dybjer (Chalmers University of Technology) Programming Languages Meet Program Verification [pdf] I will begin by giving an overview of the CoVer project (Combining Verification Methods in Software Development, 2003-2005) at Chalmers University. This was a research project comprising both researchers in Programming Languages (especially in functional programming) and Program Verification (especially in random testing, automatic theorem proving, type theory, and proof assistants). The goal of this project was to provide an environment for Haskell programming which provides access to tools for automatic and interactive correctness proofs as well as to tools for testing. I will both say something about the contributions and about the difficulties we had in fully realizing our goal. I will also give my view of some of the main scientific issues underlying the project. In particular I will say something about why it became important to understand the relationship between the "integrated" (propositions-as-types-based) and "external" approach to program verification. In the second part of the talk I will illustrate this issue by an example: the proof of correctness of a Haskell program which normalizes terms and types in Martin-Löf type theory with one universe.

10:00‑10:30

James Caldwell (University of Wyoming) Josef Pohl (Computer Science Dept. University of Wyoming) Constructive membership predicates as index types In the constructive setting, membership predicates over recursive types are inhabited by terms indexing the elements that satisfy the criteria for membership. In this paper, we motivate and explore this idea in the concrete setting of lists and trees. We show that the inhabitants of membership predicates are precisely the inhabitants of a generic shape type. We show that membership of $x$ (of type $T$) in structure $S$, $(x\in_T{}S)$ can not, in general, index all parts of a structure $S$ and we generalize to a form $\rho\in{}S$ where $\rho$ is a predicate over $S$. Under this scheme, $(\lambda{}x.True)\in{}S$ is the set of all indexes into $S$, but we show that not all subsets of indexes are expressible by strictly local predicates. Accordingly, we extend our membership predicates to predicates that retain state ``from above'' as well as allow ``looking below''. Predicates of this form are complete in the sense that they can express every subset of indexes in $S$. These ideas are motivated by experience programming in Nuprl's constructive type theory and the theorems for lists and trees have been formalized and mechanically checked.

Break (10:30‑11:00)

Session 2: Verified Programming in Haskell (11:00‑12:30)

11:00‑11:30	Martin Sulzmann (National University of Singapore) Razvan Voicu (National University of Singapore) Language-Based Program Verification via Expressive Types Recent developments in the area of expressive types have the prospect to supply the ordinary programmer with a programming language rich enough to verify complex program properties. Program verification is made possible via tractable type checking. We explore this possibility by considering two specific examples; verifying sortedness and resource usage verification. We show that advanced type error diagnosis methods become essential to assist the user in case of type checking failure. Our results point out new research directions for the development of programming environments in which users can write and verify their programs.
11:30‑12:00	Oleg Kiselyov (FNMOC, Monterey, CA) Chung-chieh Shan (Rutgers University) Lightweight static capabilities We describe a modular programming style that harnesses modern type systems to verify safety conditions in practical systems. This style has three ingredients. (1) A compact kernel of trust that is specific to the problem domain. (2) Unique names (_capabilities_) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application. (3) Static (type) proxies for dynamic values. We illustrate our approach using examples from the dependent-type literature, but our programs are written in Haskell or OCaml today, so our techniques are compatible with imperative code, native mutable arrays, and general recursion. The three ingredients of this programming style call for (1) an expressive core language, (2) type eigenvariables, and (3) phantom types.
12:00‑12:30	Louis-Julien Guillemette (Université de Montréal) Stefan Monnier (Université de Montréal) Statically Verified Type-Preserving Code Transformations in Haskell The use of typed intermediate languages can significantly increase the reliability of a compiler. By type-checking the code produced at each transformation stage, one can identify bugs in the compiler that would otherwise be much harder to find. We propose to take the use of types in compilation a step further by verifying that the transformation itself is type correct, in the sense that it is impossible that it produces an ill typed term given a well typed term as input. We base our approach on higher-order abstract syntax (HOAS), a representation of programs where variables in the object language are represented by meta-variables. We use a representation that accounts for the object language's type system using generalized algebraic data types (GADTs). In this way, the full binding and type structure of the object language is exposed to the host language's type system. In this setting we encode a type preservation property of a CPS conversion in Haskell's type system, using witnesses of a type correctness proof encoded as values in a GADT.

Lunch break (12:30‑14:00)

Session 3: Verification Environments (14:00‑15:30)

14:00‑14:30	Tim Sheard (Portland State University) Type-level Computation Using Narrowing in Omega Omega is a language with an infinite hierarchy of computational levels: value, type, kind, sort, etc. Computation at the value level is performed by reduction, and is largely unconstrained. Computation at all higher levels is performed by narrowing, and is constrained in several ways. First, all ``data" at the type level and above is inductively defined data. Second, functions at the type level and above must be inductively sequential. This is a constraint on the form of the definition, not on the expressiveness of the language. Terms at each level are classified by terms at the next level. Thus values are classified by types, types are classified by kinds, kinds are classified by sorts, etc. We maintain a strict phase distinction -- the classification of a term at level n cannot depend upon terms at lower levels. Programmers are allowed to introduce new terms and functions at every level, but any particular program will have terms at only a finite number of levels. We formalize properties of programs by exploiting the Curry-Howard isomorphism. Terms at computational level n, are used as proofs about terms at level (n+1).
14:30‑15:00	Andreas Schlosser (Technische Universität Darmstadt) Christoph Walther (Technische Universität Darmstadt) Michael Gonder Markus Aderhold (TU Darmstadt) Context-Dependent Procedures and Computed Types in VeriFun We present two enhancements of the functional language L which is used in the VeriFun system to write programs and formulate statements about them. Context-dependent procedures allow the specification of the context under which procedures are sensibly executed, thus avoiding program code with runtime tests. This also facilitates verification of absence of exceptions by proving stuck-freeness of procedure calls. Computed types lead to more compact code, increase readability of programs, and make the wellknown benefits of type systems available to non-freely generated data types as well. Since satisfaction of context requirements as well as type checking becomes undecidable, proof obligations are synthesized to be proved by the verifier at hand, thus supporting static code analysis. Information about the type hierarchy is utilized for increasing performance and efficiency of the verifier.
15:00‑15:30	Brigitte Pientka (McGill University) Functional programming with higher-order abstract syntax and explicit substitution This paper outlines a foundation for programming with higher-order abstract syntax and explicit substitutions based on contextual modal type theory \cite{Nanevski:ICML05}. Contextual modal types not only allows us to cleanly separate the representation of data objects from computation, but allow us to recurse over data objects with free variables. In this paper, we extend these ideas even further by adding first-class contexts and substitutions so that a program can pass and access code with free variables and an explicit environment, and link them in a type-safe manner. We sketch the static and operational semantics of this language, and give several examples which illustrate these features.

Break (15:30‑16:00)

Session 4: Short Papers (16:00‑16:30)

16:00‑16:15

Aaron Stump (Washington University in St. Louis) The Alternation Calculus This short paper describes work in progress on a program logic called the Alternation Calculus. This system extends an untyped lambda-calculus with an idealized operator which dualizes termination and non-termination. The alternation ~ M converges with a non-deterministically chosen value if all (non-deterministic) computations of M diverge, and diverges if M has a converging computation. Standard logical operators and type operators can be defined as terms using alternation.

16:15‑16:30

Adam Chlipala (UC Berkeley CS Division) Position Paper: Thoughts on Programming with Proof Assistants I argue that interactive proof assistants like Coq already provide very good support for PLPV-style programming. I discuss the main traditional programming language features that it lacks and why I haven't missed them much in my experiences implementing certified program analysis tools, and I summarize some of Coq's most attractive features for this domain. My overall message is that having a small language with no unnecessary distinctions between programs and proofs has a number of benefits, that Coq provides one such language, and that we should focus on proof automation and other ways of making Coq-like tools easier to use rather than create new languages from scratch.

Panel Discussion: Future Directions of Language-Based Program Verification (16:30‑17:15)