# LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue).
If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

## Past Seminars

### Realizability: denotational semantics for correctness

- Date
- Tuesday, November 07 2017 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Valentin Blot (LRI, Université Paris-Sud)

There exists a large spectrum of techniques for proving correctness of
computer programs. At one end is the Curry-Howard isomorphism, in which
a typing procedure automatically checks the correctness of a program,
and at the other end are techniques à la Hoare, in which non-trivial
reasonning is performed in a logic adapted to the programming language.
Realizability can be seen as a mixture of these two approaches: proving
that a program realizes a specification is done via a combination of
automatic techniques in a Curry-Howard fashion, and manual proofs of
correctness of subprograms with respect to some axioms. In my talk I
will present some realizability models where the realizability relation
is defined semantically: a program realizes a specification if its
denotation satisfies a property in the model. The denotational models
involved include game semantics, continuation models and Scott domains.