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
Two major approaches were to be considered:
- Operationally-based methods, studying theories of program equivalence
that are based directly upon operational semantics.
- Axiomatic methods, considering the problem of designing
logics and type theories that axiomatise salient properties of
mathematical models of computation.
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
- 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),
- 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.
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,
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
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