Sites Inria

Version française

TYPICAL Research team

TYPICAL team publications

2013

Journal articles

titre
Non-idempotent intersection types and strong normalisation
auteur
Alexis Bernadet, Stéphane Graham-Lengrand
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (4), pp.17-42
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00906778/file/Journal13.pdf BibTex

Conference papers

titre
Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation
auteur
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner
article
European Control Conference (ECC'13), Jul 2013, Zurich, Switzerland. pp.2244 - 2250, 2013
Accès au bibtex
https://arxiv.org/pdf/1307.7002 BibTex
titre
Certification of Bounds of Non-linear Functions: the Templates Method
auteur
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner
article
Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteige. Conferences on Intelligent Computer Mathematics (CICM 2013), Jul 2013, Bath, United Kingdom. Springer Berlin Heidelberg, 7961, pp.51-65, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39320-4_4〉
Accès au bibtex
https://arxiv.org/pdf/1307.3231 BibTex
titre
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
auteur
Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
article
MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363, 2013
Accès au bibtex
BibTex
titre
Extended Resolution as Certificates for Propositional Logic
auteur
Chantal Keller
article
Blanchette, Jasmin Christian and Josef Urban. PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00836845/file/keller-pxtp13.pdf BibTex

Theses

titre
A Matter of Trust: Skeptical Communication Between Coq and External Provers
auteur
Chantal Keller
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00838322/file/thesis-keller.pdf BibTex

2012

Journal articles

titre
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
auteur
Cyril Cohen, Assia Mahboubi
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. 〈10.2168/LMCS-8 (1:02) 2012〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00593738/file/1201.3731.pdf BibTex

Conference papers

titre
Parametricity in an Impredicative Sort
auteur
Chantal Keller, Marc Lasson
article
Patrick Cégielski and Arnaud Durand. CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012, Sep 2012, Fontainebleau, France. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 16, pp.381-395, 2012, CSL. 〈10.4230/LIPIcs.CSL.2012.399〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00730913/file/paramath.pdf BibTex
titre
Construction of real algebraic numbers in Coq
auteur
Cyril Cohen
article
Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00671809/file/main.pdf BibTex
titre
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
auteur
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
article
Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, 〈10.1007/978-3-642-31365-3_8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00687640/file/main.pdf BibTex
titre
The Refined Calculus of Inductive Construction: Parametricity and Abstraction
auteur
Chantal Keller, Marc Lasson
article
LICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnik, Croatia. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00757620/file/paramath.pdf BibTex
titre
Construction des nombres algébriques réels en Coq
auteur
Cyril Cohen
article
JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00665965/file/paper_11.pdf BibTex
titre
Pseudo-Weight: Making Tabletop Interaction with Virtual Objects More Tangible
auteur
Chantal Keller, Jérémy Bluteau, Renaud Blanch, Sabine Coquillart
article
Proceedings of the 2012 ACM international conference on Interactive Tabletops and Surfaces (ITS 2012), 2012, Cambridge, MA, United States. pp.201-204, 2012, 〈10.1145/2396636.2451335〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00953336/file/ITS12-PseudoWeight-Keller.pdf BibTex

Reports

titre
Two simulations about DPLL(T)
auteur
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
article
2012
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00690044/file/Main.pdf BibTex

Theses

titre
Formalized algebraic numbers: construction and first-order theory.
auteur
Cyril Cohen
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00780446/file/main.pdf BibTex

Preprints, Working Papers, ...

titre
Simulating the DPLL(T ) procedure in a sequent calculus with focusing
auteur
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
article
2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00690392/file/MainHal.pdf BibTex

2011

Journal articles

titre
A formal study of Bernstein coefficients and polynomials
auteur
Yves Bertot, Frédérique Guilhot, Assia Mahboubi
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, 21 (04), pp.731-761. 〈10.1017/S0960129511000090〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00503017/file/check_version_Jan_2011.pdf BibTex
titre
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
auteur
Germain Faure, Chantal Keller, Thery Laurent, Gregoire Benjamin, Werner Benjamin, Armand Mickael
article
CERTIFIED PROGRAMS AND PROOFS, Springer, 2011
Accès au bibtex
BibTex

Conference papers

titre
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
auteur
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Thery, Benjamin Werner
article
Jouannaud, Jean-Pierre and Shao, Zhong. CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. Springer, 7086, pp.135-150, 2011, Lecture notes in computer science - LNCS. 〈10.1007/978-3-642-25379-9_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00639130/file/cpp11.pdf BibTex
titre
Les quatre concepts de l'informatique
auteur
Gilles Dowek
article
Georges-Louis Baron, Éric Bruillard, Vassilis Komis. Sciences et technologies de l'information et de la communication en milieu éducatif : Analyse de pratiques et enjeux didactiques., Oct 2011, Patras, Grèce. Athènes : New Technologies Editions, pp.21-29, 2011, 〈ISBN : 978-960-6759-75-8〉
Accès au texte intégral et bibtex
https://edutice.archives-ouvertes.fr/edutice-00676169/file/DowekDidapro2011.pdf BibTex
titre
Communications Invitées - Colloque DIDAPRO 4 - Dida&STIC
auteur
Paul Spirakis, Georges-Louis Baron, Gilles Dowek, Eric Bruillard, Maurice Nivat
article
Georges-Louis Baron, Éric Bruillard, Vassilis Komis. Sciences et technologies de l'information et de la communication en milieu éducatif : Analyse de pratiques et enjeux didactiques., Oct 2011, Patras, Grèce. Athènes : New Technologies Editions, pp.15-47, 2011, 〈ISBN : 978-960-6759-75-8〉
Accès au texte intégral et bibtex
https://edutice.archives-ouvertes.fr/edutice-00676274/file/Communications-invitees.pdf BibTex
titre
Clausal Presentation of Theories in Deduction Modulo
auteur
Jianhua Gao
article
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00614251/file/Gao.pdf BibTex
titre
Verifying SAT and SMT in Coq for a fully automated decision procedure
auteur
Mickaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Wener
article
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00614041/file/ArmandAl.pdf BibTex
titre
CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory
auteur
Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang
article
Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011, Jun 2011, Toronto, Canada. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00583136/file/coq-mtu-lics-2011.pdf BibTex

Theses

titre
Verified Computing in Homological Algebra
auteur
Arnaud Spiwack
article
Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00605836/file/thesis.spiwack.pdf BibTex
titre
Conception d'un noyau de vérification de preuves pour le λΠ-calcul modulo
auteur
Mathieu Boespflug
article
Logique en informatique [cs.LO]. Ecole Polytechnique X, 2011. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00672699/file/thesis.pdf BibTex

Preprints, Working Papers, ...

titre
A Generic Formalised Framework for Reasoning About Weak Memory Models
auteur
Jade Alglave, Assia Mahboubi
article
2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00604656/file/itp.pdf BibTex

2010

Journal articles

titre
Extending FeatherTrait Java with Interfaces
auteur
Luigi Liquori, Arnaud Spiwack
article
Theoretical Computer Science, Elsevier, 2010, Theoretical Computer Science, 30 (1-3), pp.243-260. 〈10.1016/j.tcs.2008.01.051〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432540/file/TCS-60.pdf BibTex
titre
Les ingrédients des algorithmes
auteur
Gilles Dowek, Thierry Vieville, Jean-Pierre Archambault, Emmanuel Baccelli, Benjamin Wack
article
Interstices, INRIA, 2010, 〈https://interstices.info/jcms/c_43821/les-ingredients-des-algorithmes〉
Accès au bibtex
BibTex
titre
Tout a un reflet numérique
auteur
Gilles Dowek, Thierry Vieville, Jean-Pierre Archambault, Emmanuel Baccelli, Benjamin Wack
article
Interstices, INRIA, 2010, 〈https://interstices.info/jcms/c_43823/tout-a-un-reflet-numerique〉
Accès au bibtex
BibTex
titre
An introduction to small scale reflection in Coq
auteur
Georges Gonthier, Assia Mahboubi
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2010, 3 (2), pp.95-152
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00515548/file/main-rr.pdf BibTex

Conference papers

titre
Hereditary Substitutions for Simple Types, Formalized
auteur
Chantal Keller, Thorsten Altenkirch
article
Capretta, V. and Chapman, J. MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States. ACM Press, 2010, Proceedings of the Mathematically Structured Functional Programming workshop, ACM Press 2010, Baltimore, Marylan, USA, September 25, 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00520606/file/msfp10.pdf BibTex
titre
An abstract type for constructing tactics in Coq
auteur
Arnaud Spiwack
article
Proof Search in Type Theory, Jul 2010, Edinburgh, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00502500/file/tactics.pdf BibTex
titre
Extending Coq with Imperative Features and its Application to SAT Verification
auteur
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry
article
Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00502496/file/fastcoq.pdf BibTex
titre
A formal quantifier elimination for algebraically closed fields
auteur
Cyril Cohen, Assia Mahboubi
article
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science. 〈10.1007/978-3-642-14128-7_17〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00464237/file/main.pdf BibTex
titre
Importing HOL Light into Coq
auteur
Chantal Keller, Benjamin Werner
article
Matt Kaufmann and Lawrence C. Paulson. ITP - Interactive Theorem Proving, First International Conference - 2010, Jul 2010, Edimbourg, United Kingdom. Springer, 6172, pp.307-322, 2010, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/a74714134ut7316n/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00520604/file/itp10.pdf BibTex
titre
Conversion by Evaluation
auteur
Mathieu Boespflug
article
Twelfth International Symposium on Practical Aspects of Declarative Languages, Jan 2010, Madrid, Spain. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00434282/file/derivesn.pdf BibTex

Book sections

titre
Constructively Finite?
auteur
Arnaud Spiwack, Thierry Coquand
article
Lambán Pardo, Laureano and Romero Ibáñez, Ana and Rubio García, Julio. Contribuciones científicas en honor de Mirian Andrés Gómez, Universidad de La Rioja, pp.217-230, 2010, 978-84-96487-50-5
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00503917/file/Coquand_Spiwack_-_2010_-_Constructively_Finite.pdf BibTex

Preprints, Working Papers, ...

titre
Formalizing real analysis for polynomials
auteur
Cyril Cohen
article
2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00545778/file/main.pdf BibTex

2009

Journal articles

titre
À propos de l’enseignement de l’informatique
auteur
Gilles Dowek, Joanna Jongwane
article
Interstices, INRIA, 2009
Accès au bibtex
BibTex
titre
La vérité et la machine
auteur
Benjamin Werner
article
Interstices, INRIA, 2009, 〈https://interstices.info/jcms/c_42623/la-verite-et-la-machine〉
Accès au bibtex
BibTex

Conference papers

titre
Efficient normalization by evaluation
auteur
Mathieu Boespflug
article
Olivier Danvy. 2009 Workshop on Normalization by Evaluation, Aug 2009, Los Angeles, United States. 2009, 〈http://www.brics.dk/~danvy/NBE09/informal-proceedings/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00434283/file/NBE09-Boespflug-fastnbe.pdf BibTex
titre
From Self-Interpreters to Normalization by Evaluation
auteur
Mathieu Boespflug
article
Olivier Danvy. 2009 Workshop on Normalization by Evaluation, Aug 2009, Los Angeles, United States. 2009, 〈http://www.brics.dk/~danvy/NBE09/informal-proceedings/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00434284/file/selfnbe.pdf BibTex
titre
Complete reducibility candidates
auteur
Denis Cousineau
article
Proof Search in Type Theory, Aug 2009, Montréal, Canada. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00433159/file/CompleteReducibilityCandidates.pdf BibTex
titre
Packaging Mathematical Structures
auteur
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
article
Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, 2009, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00368403/file/main.pdf BibTex

Reports

titre
A Categorical Semantics for The Parallel Lambda-Calculus
auteur
Germain Faure, Alexandre Miquel
article
[Research Report] RR-7063, INRIA. 2009, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00424248/file/RR-7063.pdf BibTex
titre
Encoding rewriting strategies in lambda-calculi with patterns
auteur
Germain Faure
article
[Research Report] RR-7025, INRIA. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00413178/file/rapport.pdf BibTex
titre
Higher-order matching modulo (super)developements. Applications to second-order matching
auteur
Germain Faure
article
[Research Report] 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00429978/file/matching.pdf BibTex

Theses

titre
Modèles et normalisation des preuves
auteur
Denis Cousineau
article
Informatique [cs]. Ecole Polytechnique X, 2009. Français
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-00433165/file/manuscript.pdf BibTex

Preprints, Working Papers, ...

titre
A completeness theorem for strong normalization in minimal deduction modulo
auteur
Denis Cousineau
article
2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00370379/file/CompletenessMDM.pdf BibTex
titre
A semantic method to prove strong normalization from weak normalization
auteur
Denis Cousineau
article
2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00385520/file/RiceSaladLambdaModulo.pdf BibTex

2008

Journal articles

titre
FeatherTrait: A Modest Extension of Featherweight Java
auteur
Luigi Liquori, Arnaud Spiwack
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2008, ACM Transactions on Programming Languages and Systems (TOPLAS), 30 (2), pp.11:1--11:32. 〈10.1145/1330017.1330022〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432538/file/fjtraits.pdf BibTex

Conference papers

titre
The computability path ordering: the end of a quest
auteur
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
article
7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy. 5213, 2008, LNCS
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00288209/file/main.pdf BibTex
titre
Catch me if you can Looking for type-safe, hierarchical, lightweight, polymorphic and efficient error management in OCaml
auteur
David Teller, Arnaud Spiwack, Till Varoquaux
article
IFL 2008, Sep 2008, Hertfordshire, United Kingdom. 21 p., 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432575/file/monad.pdf BibTex
titre
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
auteur
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
article
5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Sep 2008, Milan, Italy. 273, 2008, IFIP. 〈10.1007/978-0-387-09680-3_24〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00275382/file/main.pdf BibTex
titre
The Implicit Calculus of Constructions as a Programming Language with Dependent Types
auteur
Bruno Barras, Bruno Bernardo
article
FoSSaCS, Mar 2008, Budapest, Hungary. pp.365-379, 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00429543/file/icc_barras_bernardo.pdf BibTex
titre
A New Elimination Rule for the Calculus of Inductive Constructions
auteur
Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Sacchini
article
Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro. Types for Proofs and Programs, Mar 2008, Torino, Italy. Springer, 5497, pp.32-48, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02444-3_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00524938/file/types-BarCorGreHerSac08-dep-matching.pdf BibTex
titre
An Approach to Call-by-Name Delimited Continuations
auteur
Hugo Herbelin, Silvia Ghilezan
article
George C. Necula and Philip Wadler. Symposium on Principles of Programming Languages, Jan 2008, San Francisco, United States. ACM, pp.383-394, 2008, SIGPLAN-SIGACT. 〈10.1145/1328438.1328484〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00524949/file/popl-HerGhi08-cbn-delim.pdf BibTex

Reports

titre
Permissive nominal terms
auteur
Gilles Dowek, Murdoch Gabbay, Dominic Mulligan
article
[Research Report] RR-6682, INRIA. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00335115/file/RR-6682.pdf BibTex

Theses

titre
Type Theory and Decision Procedures
auteur
Pierre-Yves Strub
article
Formal Languages and Automata Theory [cs.FL]. Ecole Polytechnique X, 2008. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-00351837/file/manuscrit.pdf BibTex

2007

Journal articles

titre
Preuves formelles, preuves calculatoires
auteur
Benjamin Werner
article
Interstices, INRIA, 2007, 〈https://interstices.info/jcms/c_23115/preuves-formelles-preuves-calculatoires〉
Accès au bibtex
BibTex
titre
A Proof of Strong Normalisation Using Domain Theory
auteur
Thierry Coquand, Arnaud Spiwack
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2007, 16 p. 〈10.2168/LMCS-3(4:12)2007〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432448/file/sn4.pdf BibTex

Conference papers

titre
The Implicit Calculus of Constructions as a Programming Language with Dependent Types
auteur
Bruno Barras, Bruno Bernardo
article
International Workshop on Type theory, proof theory, and rewriting (TPR'07), Jun 2007, Paris, France. 2007, 〈http://www.lix.polytechnique.fr/~dowek/tpr.html〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432658/file/icc_barras_bernardo-tpr07.pdf BibTex
titre
Towards Constructive Homological Algebra in Type Theory
auteur
Thierry Coquand, Arnaud Spiwack
article
CALCULEMUS 2007, Jun 2007, Hagenberg, Austria. 12 p., 2007, 〈10.1007/978-3-540-73086-6_4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432525/file/v2.pdf BibTex

2006

Journal articles

titre
L’engagement des scientifiques
auteur
Gilles Dowek
article
Interstices, INRIA, 2006, 〈https://interstices.info/jcms/c_19051/l-engagement-des-scientifiques〉
Accès au bibtex
BibTex

Conference papers

titre
A Proof of Strong Normalisation using Domain Theory
auteur
Thierry Coquand, Arnaud Spiwack
article
LICS 2006, Aug 2006, Seatle, United States. 10 p., 2006, 〈10.1109/LICS.2006.8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432490/file/sn2.pdf BibTex