Publications de l'équipe TYPICAL

2012

Articles dans des revues avec comité de lecture

Titre

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

Auteurs

Cyril Cohen; Assia Mahboubi

Détail

Logical Methods in Computer Science, IfCoLog (International Federation of Computational Logic), 2012, 8 (1:02), pp. 1-40

Accès au texte intégral et bibtex

Communications avec actes

Titre

Pseudo-Weight: Making Tabletop Interaction with Virtual Objects More Tangible

Auteurs

Chantal Keller ; Renaud Blanch

Détail

ITS - ACM International Conference on Interactive Tabletops and Surfaces - 2012, Nov 2012, Cambridge, United States.

Accès au texte intégral et bibtex

Titre

Parametricity in an Impredicative Sort

Auteurs

Chantal Keller ; Marc Lasson

Détail

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, CSL, 16, pp. 381-395

Accès au texte intégral et bibtex

Titre

Construction of real algebraic numbers in Coq

Auteurs

Cyril Cohen

Détail

Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer

Accès au texte intégral et bibtex

Titre

Construction des nombres algébriques réels en Coq

Auteurs

Cyril Cohen

Détail

JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France.

Accès au texte intégral et bibtex

Titre

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic

Auteurs

François Bobot; Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala; Assia Mahboubi; Alain Mebsout; Guillaume Melquiond

Détail

Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, Automated Reasoning, 7364, pp. 67-81, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Communications sans actes

Titre

The Refined Calculus of Inductive Construction: Parametricity and Abstraction

Auteurs

Chantal Keller ; Marc Lasson

Détail

LICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnik, Croatia.

Accès au texte intégral et bibtex

Rapports

Titre

Two simulations about DPLL(T)

Auteurs

Mahfuza Farooque; Stéphane Lengrand ; Assia Mahboubi

Détail

[Report], 2012

Accès au bibtex

Documents sans référence de publication

Titre

Simulating the DPLL(T ) procedure in a sequent calculus with focusing

Auteurs

Mahfuza Farooque; Stéphane Lengrand ; Assia Mahboubi

Détail

Apr. 2012

Accès au texte intégral et bibtex

2011

Articles dans des revues avec comité de lecture

Titre

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Auteurs

Germain Faure ; Chantal Keller; Thery Laurent; Gregoire Benjamin; Werner Benjamin; Armand Mickael

Détail

CERTIFIED PROGRAMS AND PROOFS, Springer, 2011

Accès au bibtex

Titre

A formal study of Bernstein coefficients and polynomials

Auteurs

Yves Bertot; Frédérique Guilhot; Assia Mahboubi

Détail

Mathematical Structures in Computer Science, Cambridge University Press, 2011, 21 (04), pp. 731-761

Accès au texte intégral et bibtex

Communications avec actes

Titre

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Auteurs

Michaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Thery; Benjamin Werner

Détail

Jouannaud, Jean-Pierre and Shao, Zhong. CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan, Province Of China. Springer, Certified Programs and Proofs, 7086, pp. 135-150, Lecture notes in computer science - LNCS

Accès au texte intégral et bibtex

Titre

CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory

Auteurs

Bruno Barras; Jean-Pierre Jouannaud; Pierre-Yves Strub; Qian Wang

Détail

Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011, Jun 2011, Toronto, Canada.

Accès au texte intégral et bibtex

Titre

Verifying SAT and SMT in Coq for a fully automated decision procedure

Auteurs

Mickaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Théry; Benjamin Wener

Détail

PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland.

Accès au texte intégral et bibtex

Titre

Clausal Presentation of Theories in Deduction Modulo

Auteurs

Jianhua Gao

Détail

PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland.

Accès au texte intégral et bibtex

Thèses

Titre

Calculs vérifiés en algèbre homologique

Auteurs

Arnaud Spiwack

Détail

Informatique. Ecole Polytechnique X, Mar. 2011. English

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

A Generic Formalised Framework for Reasoning About Weak Memory Models

Auteurs

Jade Alglave; Assia Mahboubi

Détail

Jun. 2011

Accès au texte intégral et bibtex

Titre

A constructive version of Laplace's proof on the existence of complex roots

Auteurs

Cyril Cohen; Thierry Coquand

Détail

May. 2011

Accès au texte intégral et bibtex

2010

Articles dans des revues avec comité de lecture

Titre

An introduction to small scale reflection in Coq

Auteurs

Georges Gonthier; Assia Mahboubi

Détail

Journal of Formalized Reasoning, Journal of Formalized Reasoning, 2010, 3 (2), pp. 95-152

Accès au texte intégral et bibtex

Communications avec actes

Titre

A formal quantifier elimination for algebraically closed fields

Auteurs

Cyril Cohen; Assia Mahboubi

Détail

Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, Intelligent Computer Mathematics, 6167, pp. 189-203, Computer Science

Accès au texte intégral et bibtex

Titre

Conversion by Evaluation

Auteurs

Mathieu Boespflug

Détail

Twelfth International Symposium on Practical Aspects of Declarative Languages, Jan 2010, Madrid, Spain.

Accès au texte intégral et bibtex

Titre

Extending Coq with Imperative Features and its Application to SAT Verification

Auteurs

Michaël Armand; Benjamin Grégoire; Arnaud Spiwack; Laurent Théry

Détail

Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Titre

An abstract type for constructing tactics in Coq

Auteurs

Arnaud Spiwack

Détail

Proof Search in Type Theory, Jul 2010, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Titre

Importing HOL Light into Coq

Auteurs

Chantal Keller; Benjamin Werner

Détail

Matt Kaufmann and Lawrence C. Paulson. ITP - Interactive Theorem Proving, First International Conference - 2010, Jul 2010, Edimbourg, United Kingdom. Springer, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, 6172, pp. 307-322, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Hereditary Substitutions for Simple Types, Formalized

Auteurs

Chantal Keller; Thorsten Altenkirch

Détail

Capretta, V. and Chapman, J.. MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States. ACM Press, 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

Chapitres d'ouvrages scientifiques

Titre

Constructively Finite?

Auteurs

Arnaud Spiwack; Thierry Coquand

Détail

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

Documents sans référence de publication

Titre

Formalizing real analysis for polynomials

Auteurs

Cyril Cohen

Détail

Dec. 2010

Accès au texte intégral et bibtex

2009

Communications avec actes

Titre

Complete reducibility candidates

Auteurs

Denis Cousineau

Détail

Proof Search in Type Theory, Aug 2009, Montréal, Canada.

Accès au texte intégral et bibtex

Titre

Packaging Mathematical Structures

Auteurs

François Garillot; Georges Gonthier; Assia Mahboubi; Laurence Rideau

Détail

Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

A New Elimination Rule for the Calculus of Inductive Constructions

Auteurs

Bruno Barras; Pierre Corbineau; Benjamin Grégoire; Hugo Herbelin; Jorge Sacchini

Détail

Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro. Types for Proofs and Programs, Mar 2008, Torino, Italy. Springer, Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, 5497, pp. 32-48, 2009, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Communications sans actes

Titre

Efficient normalization by evaluation

Auteurs

Mathieu Boespflug

Détail

Olivier Danvy. 2009 Workshop on Normalization by Evaluation, Aug 2009, Los Angeles, United States.

Accès au texte intégral et bibtex

Titre

From Self-Interpreters to Normalization by Evaluation

Auteurs

Mathieu Boespflug

Détail

Olivier Danvy. 2009 Workshop on Normalization by Evaluation, Aug 2009, Los Angeles, United States.

Accès au texte intégral et bibtex

Rapports

Titre

Encoding rewriting strategies in lambda-calculi with patterns

Auteurs

Germain Faure

Détail

[Research Report], 2009. RR-7025

Accès au texte intégral et bibtex

Titre

A Categorical Semantics for The Parallel Lambda-Calculus

Auteurs

Germain Faure; Alexandre Miquel

Détail

[Research Report], 2009, pp. 22. RR-7063

Accès au texte intégral et bibtex

Titre

Higher-order matching modulo (super)developements. Applications to second-order matching

Auteurs

Germain Faure

Détail

[Research Report], 2009

Accès au texte intégral et bibtex

Thèses

Titre

Modèles et normalisation des preuves

Auteurs

Denis Cousineau

Détail

Ecole Polytechnique X, Dec. 2009. French

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

A completeness theorem for strong normalization in minimal deduction modulo

Auteurs

Denis Cousineau

Détail

Mar. 2009

Accès au texte intégral et bibtex

Titre

A semantic method to prove strong normalization from weak normalization

Auteurs

Denis Cousineau

Détail

2009

Accès au texte intégral et bibtex

2008

Articles dans des revues avec comité de lecture

Titre

FeatherTrait: A Modest Extension of Featherweight Java

Auteurs

Luigi Liquori; Arnaud Spiwack

Détail

ACM Transactions on Programming Languages and Systems, ACM, 2008, 32 p.

Accès au texte intégral et bibtex

Titre

Extending FeatherTrait Java with Interfaces

Auteurs

Luigi Liquori; Arnaud Spiwack

Détail

Theoretical Computer Science, Elsevier, 2008

Accès au texte intégral et bibtex

Communications avec actes

Titre

From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures

Auteurs

Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub

Détail

5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Sep 2008, Milan, Italy. 273, IFIP

Accès au texte intégral et bibtex

Titre

The Implicit Calculus of Constructions as a Programming Language with Dependent Types

Auteurs

Bruno Barras; Bruno Bernardo

Détail

FoSSaCS, Mar 2008, Budapest, Hungary. pp. 365-379

Accès au texte intégral et bibtex

Titre

Catch me if you can Looking for type-safe, hierarchical, lightweight, polymorphic and efficient error management in OCaml

Auteurs

David Teller; Arnaud Spiwack; Till Varoquaux

Détail

IFL 2008, Sep 2008, Hertfordshire, United Kingdom. 21 p.

Accès au texte intégral et bibtex

Conférences invitées

Titre

The computability path ordering: the end of a quest

Auteurs

Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio

Détail

7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy. 5213, LNCS

Accès au texte intégral et bibtex

Rapports

Titre

A Small Scale Reflection Extension for the Coq system

Auteurs

Georges Gonthier; Assia Mahboubi; Enrico Tassi

Détail

[Research Report], 2008. RR-6455

Accès au texte intégral et bibtex

Thèses

Titre

Théorie des Types et Procédures de Décision

Auteurs

Pierre-Yves Strub

Détail

Ecole Polytechnique X, Jul. 2008. English

Accès au texte intégral et bibtex

2007

Articles dans des revues avec comité de lecture

Titre

A Proof of Strong Normalisation Using Domain Theory

Auteurs

Thierry Coquand; Arnaud Spiwack

Détail

Logical Methods in Computer Science (LMCS), 2007, 16 p.

Accès au texte intégral et bibtex

Communications avec actes

Titre

Towards Constructive Homological Algebra in Type Theory

Auteurs

Thierry Coquand; Arnaud Spiwack

Détail

CALCULEMUS 2007, Jun 2007, Hagenberg, Austria. 12 p.

Accès au texte intégral et bibtex

Titre

The Implicit Calculus of Constructions as a Programming Language with Dependent Types

Auteurs

Bruno Barras; Bruno Bernardo

Détail

International Workshop on Type theory, proof theory, and rewriting (TPR'07), Jun 2007, Paris, France.

Accès au texte intégral et bibtex

2006

Communications avec actes

Titre

A Proof of Strong Normalisation using Domain Theory

Auteurs

Thierry Coquand; Arnaud Spiwack

Détail

LICS 2006, Aug 2006, Seatle, United States. 10 p.

Accès au texte intégral et bibtex