**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:- 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.

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.

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