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

			     S E M I N A I R E
			   __                                  
			  / _`  _   /  /  o           
			 /   ) __) /  /  / /  / /\/| 
			(___/ (_/ (_ (_ / (__/ /   |  
                                                
			  I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                             Lundi 29 juin, 10h30

                              -----------------
                              Filip Sieczkowski
                              -----------------

                                    INRIA

        ==============================================================
                 ModuRes: a Coq Library for Modular Reasoning
        about Concurrent Higher-Order Imperative Programming Languages
        ==============================================================

It is well-known that it is challenging to build semantic models of type
systems or logics for reasoning about concurrent higher-order imperative
programming languages. One of the key challenges is that such semantic models
often involve constructing solutions to certain kinds of recursive domain
equations, which in practice has been a barrier to formalization efforts. I
will present the ModuRes Coq library, which provides an easy way to solve such
equations, and show how the library can be used to construct models of type
systems and logics for reasoning about concurrent higher-order imperative
programming languages.