~~NOCACHE~~
---- datatemplateentry ----
template    : en:templates:equipe
type        : Thematic team
nom         : Proofs and programs
nomcourt    : preuves
responsable : saurin
pole        : pps
---- 

\\ === Research themes ===

Our methodology is based on the Curry-Howard correspondence between proofs and programs, where rewriting plays a central role, describing both cut-elimination in proof theory and operational semantics of programs. The basic object is the lambda-calculus, which is a pure theory of functional programming and of its extensions: by type systems, linear or differential refinements, pattern-matching mechanisms, or various kinds of non-purely functional computational effects (nondeterministic or probabilistic choice, continuations, local or nonlocal internal states, etc.). We thus obtain formalisms that are interesting for their logical properties, giving for example a computational interpretation of standard concepts in logic (like the choice or reductio ad absurdum). We also get abstract representations of real programming languages, in a framework that is as implementation-independent as possible, that allows semantics analysis. Among these extensions, the calculus of inductive constructions is both a logic and a programming language, on which the Coq proof assistant is based.

/*
{{ patates.svg?500 |Activités de recherche }}
*/

\\ === Seminar and working groups ===

[[::en:seminaires:pps:]] \\
[[::en:seminaires:semantique:]] \\
[[::en:seminaires:types:]]

\\ === Permanent members  ===

{{page>.:db:annuaire_perm_en}}

\\ === Non-permanent members ===

{{page>.:db:annuaire_noperm_en}}