X. Theorem-term_ind-{ctxt, Var x)) -> (forall x T t, x # C -> P t -> P (Lam x T t)) -> (forall t1 t2, Abs X T t)) -> (forall t T, P t -> P (TApp t T)) -> forall (u : term)

. De and . Qu, instances de NAST, term et typ sont automatiquement pourvus d'une fonction de substitution {x:=t} qui vérifie leséquationsleséquations attendues : ? (Var y){x:=t} = if x == y then t else Var y ? (App t1 t2){x:=t} = App t1{x:=t} t2{x:=t} ? (Lam y u){x:=t} = Lam y u{x

F. La-représentation-nominale-du-langage, permet des raisonnements formels très similaires aux raisonnements sur papier Une illustration est la solution du POPLmark Challengé ecrite avec Nominal Isabelle [UPV + 06]. On souhaiterait naturellement proposer une solution du POPLmark Challenge utilisant la librairie définie dans ce rapport

. Mais-avant-cela, il faut rendre cette librairie plus simplè a utiliser ; en particulier, les exemples précédents ont montré que la syntaxe utilisée pour définir un ensemble nominal puis une fonction récursive sur cet ensemble est verbeuse et assez inélégante

. Le-principe-d-'induction-et-l-'´-eliminateur-permettant-de-raisonner-sur-les and . Qu, ils soient immediatsàimmediatsà prouveràprouverà partir des principes généraux NAST_ind et NAST_rect, doiventêtrédoiventêtré enoncésenoncésà la main Il faudrait que ces preuves soient faites automatiquement (avec un pluginécritpluginécrit en OCAML), comme c'est le cas pour les types inductifs. De plus, pour définir une fonction avec l'´ eliminateur NAST_rect, il faut prouver que les fonctions f_var, f_cons et f_bcons sontéquivariantessontéquivariantes, ce qui est le plus souvent immédiat. Pour prouver ces résultats d'´ equivariance automatiquement, on aimerait appliquer le théorème de paramétricité [Wad89] (grâcè a un plugin paramcoqécritparamcoqécrit par Marc Lasson) en exprimant l'´ equivariance comme une relation paramétrée, Enfin, dans les preuves réalisées dans le cadre de ce travail, il est très fréquent de devoir prouver des résultats de fra??cheurfra??cheur de la forme fresh atom (x 1 , x 2 , . . . , x n ) # x i , ou bien fresh atom (. . . , f i, . . .) # f

. Actuellement, ces buts sont résolus par une tactique Ltac, mais il serait intéressant d'utiliser le mécanisme d'inférence de type des Typeclasses

R. Aydemir, A. Bohannon, and S. Weirich, Nominal Reasoning Techniques in Coq, International Workshop on Logical Frameworks and Meta-Languages :Theory and Practice (LFMTP), 2006.
DOI : 10.1016/j.entcs.2007.01.028

E. Brian and . Aydemir, Mechanized metatheory for the masses : The poplmark challenge, 2005.

H. P. Barendregt, The lambda calculus : its syntax and semantics. Studies in logic and the foundations of mathematics, 1981.

[. Giménez and &. Pierre-castéran, A tutorial on [co-]inductive types in Coq, 2007.

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, 2009.
DOI : 10.1007/s10817-011-9225-2

C. Cohen, Pragmatic Quotient Types in Coq, Interactive Theorem Proving, pp.213-228, 2013.
DOI : 10.1007/978-3-642-39634-2_17

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system, 2015.
URL : https://hal.archives-ouvertes.fr/inria-00258384

J. Girard, P. Taylor, and Y. Lafont, Proofs and Types, 1989.

M. Hofmann and T. Streicher, The groupoid interpretation of type theory, Venice Festschrift, pp.83-111, 1996.

F. Pfenning and C. Elliott, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN '88 Conference on Programming Language Design and Implementation (PLDI), pp.199-208, 1988.

C. Benjamin and . Pierce, Types and Programming Languages, 2002.

A. M. Pitts, Alpha-structural recursion and induction, Journal of the ACM, vol.53, issue.3, pp.459-506, 2006.
DOI : 10.1145/1147954.1147961

A. M. Pitts, Nominal Sets. Cambridge tracts in theoretical computer science, 2013.

M. Sozeau and O. Nicolas, First-Class Type Classes. Lecture notes in computer science, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00628864

P. Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture , FPCA '89, pp.347-359, 1989.
DOI : 10.1145/99370.99404