Theme D: Verification methods

First year Progress Report

Coordinators: Pitts and Rosolini

Partners: Aarhus (Nielsen, Winskel), Cambridge (Gordon, Hyland, Ong, Pitts), Chalmers (Dybjer, Sands), Darmstadt (Hofmann, Reus, Streicher), Edinburgh (Abramsky), Genova (Moggi, Rosolini), QMW (O'Hearn).

Our objective under this heading was to develop formal methods for reasoning about properties of programs and system behaviour based on new approaches to semantics that emerged from the previous projects. To use such theories as the basis for proofs of correctness of compilers and program optimisations, we have adapted known semantics to fit the present needs and we have studied specific languages.

Two major approaches were to be considered:
  1. Operationally-based methods, studying theories of program equivalence that are based directly upon operational semantics.
  2. Axiomatic methods, considering the problem of designing logics and type theories that axiomatise salient properties of mathematical models of computation.

Operationally-based methods

In the last few years increasing use has been made of structural operational semantics to study aspects of programming languages which traditionally have been analysed via denotational semantics. Since there are more or less adequate denotational models for programming language features such as higher order functions and procedures, recursive definitions, local state, and data abstraction, one might wonder why one should consider syntactic methods at all. Andrew Pitts attempted to explain why in an invited tutorial [Pitts (1)] at the PLILP/ALP'98 conference that took place concurrently with the APPSEM workshop in Pisa. He has applied operationally-based versions of the technique of logical relations to study polymorphic types from a functional programming perspective, where the partialness arising from the presence of fixpoint recursion complicates the nature of potentially infinite (`lazy') datatypes. An approach to Reynolds' notion of relational parametricity has been developed that works directly on the syntax of a programming language, using a novel closure operator to relate operational behaviour to parametricity properties of types; working with an extension of Plotkin's PCF with forall-types, lazy lists and existential types, Pitts shows by example how the resulting logical relation can be used to prove properties of polymorphic types up to operational equivalence [Pitts (2)]. These techniques have also been used to provide simple methods for proving equivalence of implementations of abstract datatypes (i.e. elements of existential type); in [Pitts (3)] it shown that the existence of suitable, syntactical relations is sufficient, but not necessary for proving operational equivalences at existential types.

Andrew Gordon has studied the untyped ambient calculus, and various type systems for the calculus. These type systems offer guarantees about the types of messages that may be exchanged within an ambient, about whether an ambient is mobile or not, and about whether an ambient may be dissolved or not. This work was presented at the APPSEM workshop in Pisa, September '98, and in two separate papers that will both be published this year, [Cardelli&Gordon] and [Cardellietal].

Call-by-push-value (previously defined as call-by-observable) is a new paradigm that subsumes the call-by-name and call-by-value paradigms in the following sense: both operational and denotational semantics for the latter arise from similar semantics for call-by-push-value. Paul Blain Levy has analyzed various computational effects and shown how they work within call-by-push-value. This work was presented at the APPSEM workshop in Pisa, September '98, and appeared in [Levy].

L. Cardelli, A.D. Gordon
Types for mobile ambients. Proceedings of POPL99, pp79-92, ACM Press (1999).
L. Cardelli, G. Ghelli, A.D. Gordon
Mobility types for mobile ambients. Accepted for publication in the Proceedings of ICALP99, Springer LNCS (1999).
P.B. Levy
Call-By-Push-Value: A Subsuming Paradigm (Extended Abstract). In Jean-Yves Girard (ed.), Proceedings, Typed Lambda Calculi and Applications, L'Aquila, Italy, April 1999., LNCS 1581.
A. M. Pitts (1)
Operational Versus Denotational Methods in the Semantics of Higher Order Languages. In C. Palamidessi, H. Glaser and K. Meinke (Eds), Principles of Declarative Programming, 10th Int. Symp., PLILP'98, Lecture notes in Computer Science Vol. 1490 (Springer, Berlin, 1998), pp 282-283.
A. M. Pitts (2)
Parametric Polymorphism and Operational Equivalence, Cambridge University Computer Laboratory Technical Report Number 453, December, 1998. Available from ftp://ftp.cl.cam.ac.uk/papers/ap/.(A preliminary version appeared in Proceedings, Second Workshop on Higher Order Operational Techniques in Semantics (HOOTS II), Stanford CA, December 1997, Electronic Notes in Theoretical Computer Science 10(1998).)
A. M. Pitts (3)
Existential Types: Logical Relations and Operational Equivalence. In K. Larsen, S. Skyum and G. Winskel (Eds), Proc. ICALP'98, Lecure Notes in Computer Science, Volume 1443 (Springer-Verlag, 1998), pages 309-326.

Axiomatic methods

Paul Blain Levy has further considered aspects of semantics succeeding in making rigorous the jumping aspect of the continuation semantics for CBPV (call-by-push-value, previously defined as call-by-observable). In that context, he developed a semantics for recursive types and, more generally, infinitely deep types. He is actively studying properties of functor category semantics for local store in CBPV.

The logical approach to Synthetic Domain Theory has been generalized to allow also for non Scott-domains in [Reus&Streicher] following ideas of the realisability semantics of [Longley&Simpson] and the work of [Rosolini].

It has been shown that, when the dominance S of discourse is double-negation closed, the number of axioms can be significantly reduced. The well-known principles for program verification (Fixpoint-, Park-, Computational Induction) could be derived in the generalized synthetic setting as well. Fixpoint induction works for complete focal S-spaces. For the other induction principles one needs, however, a stronger notion of admissibility than just completeness, namely orthogonality on step:N --> w. In this case Fixpoint Induction for admissible predicates can be derived from Computational Induction already for complete sets carrying a focal lift-algebra structure. Another major point is the solution of recursive domain equations in the general setting. If the underlying universe of sets is impredicative it can be achieved by a simple coding trick. For a predicative universe this is ongoing research. This work was presented at the APPSEM workshop in Pisa, September '98.

Another topic of research is the representation of terms of lambda-calculi in functional languages. In [Altenkirch&Reus] we propose a monadic representation of lambda-terms using heterogeneous datatypes. The corresponding type-operator can be extended to a Kleisli triple, which is a concise way to verify the substitution laws for lambda-calculus. One can observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. The construction can be extended to the simply typed lambda-calculus using dependent types. Contrary to Higher-Order-Abstract-Syntax one still has to verify for any appropriately defined datatype the monad laws individually, but from those the substitution laws are obtained for free and, moreover, everything remains first-order.

T. Altenkirch and B. Reus
Monadic presentations of lambda terms using generalized inductive types. Submitted, 1999
J.R. Longley and A.K. Simpson
A uniform appraoch to domain theory in realizability models. Math. Struct. in Comp. Sci Year 7(5):453-468, 1997. Special edition of MSCS for the Workshop on Logic, Domains and Programming Languages, Darmstadt, Germany
B. Reus and Th. Streicher
General Synthetic Domain Theory -- A Logical Approach. To appear in Math. Struct. in Comp. Sci.
G. Rosolini
Notes on Synthetic Domain Theory. Available from ftp://ftp.disi.unige.it/pub/person/RosoliniG/papers/. August 1995