Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E

                   ______                __    _               
                  / ____/___ _____ ___  / /_  (_)_  ______ ___ 
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ 

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 2 novembre, 14h30

                              -----------------
                              Nathanaël Courant
                              -----------------

                                 Inria Paris

                 ============================================
                 Big-step semantics for the strong λ-calculus
                 ============================================

I will present big-step semantics for the strong call-by-name λ-calculus, and
derive a call-by-need semantics from it. The key idea behind those semantics
is to parameterise them by a mode, which selects whether full strong normal
form is needed or not. The semantics are formalized in Coq and proved to be
correct with respect to β-reduction. I will also talk about the ongoing work
using those semantics to write a fast, compiled implementation of the strong
λ-calculus.

[Note from the organiser: the seminar will be accessible online via
BigBlueButton. We will send a URL shortly before the talk.]