University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > A call-by-value realizability model for PML

A call-by-value realizability model for PML

Add to your list(s) Download to your calendar using vCal

  • UserRodolphe Lepigre, Laboratoire de Mathématiques, Université de Savoie World_link
  • ClockFriday 26 February 2016, 14:00-15:00
  • HouseSS03.

If you have a question about this talk, please contact Ohad Kammar.


We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity