Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

31 résultats
Page :
triés par
Image document

Beagle as a HOL4 external ATP method

 Thibault Gauthier , Cezary Kaliszyk , Chantal Keller , Michael Norrish
PAAR - Fourth Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienne, Austria
Communication dans un congrès hal-01089316v1
Image document

SMTCoq: A plug-in for integrating SMT solvers into Coq

 Burak Ekici , Alain Mebsout , Cesare Tinelli , Chantal Keller , Guy Katz , et al.
Computer Aided Verification - 29th International Conference, Jul 2017, Heidelberg, Germany
Communication dans un congrès hal-01669345v1
Image document

HOL-TestGen Version 1.8 USER GUIDE

 Achim D. Brucker , Lukas Brügger , Abderrahmane Feliachi , Chantal Keller , Matthias P. Krieger , et al.
[Technical Report] Univeristé Paris-Saclay; LRI - CNRS, University Paris-Sud. 2016
Rapport hal-01765526v1
Image document

Parametricity in an Impredicative Sort

 Chantal Keller , Marc Lasson
CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012, Sep 2012, Fontainebleau, France. pp.381-395, ⟨10.4230/LIPIcs.CSL.2012.399⟩
Communication dans un congrès hal-00730913v1
Image document

Hereditary Substitutions for Simple Types, Formalized

 Chantal Keller , Thorsten Altenkirch
MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States
Communication dans un congrès inria-00520606v1
Image document

An Interactive SMT Tactic in Coq using Abductive Reasoning

 Haniel Barbosa , Chantal Keller , Andrew Reynolds , Arjun Viswanathan , Cesare Tinelli , et al.
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Jun 2023, Manizales, Colombia. pp.11-22, ⟨10.29007/432m⟩
Communication dans un congrès hal-04287029v1
Image document

General Automation in Coq through Modular Transformations

 Valentin Blot , Louise Dubois de Prisque , Chantal Keller , Pierre Vial
Seventh Workshop on Proof Exchange in Theorem Proving, Jul 2021, Pittsburgh, United States. ⟨10.4204/EPTCS.336.3⟩
Communication dans un congrès hal-03328935v1
Image document

JFLA 2021 - 32 èmes Journées Francophones des Langages Applicatifs

 Yann Regis-Gianas , Chantal Keller
2021
Ouvrages hal-03190426v2
Image document

Bécassine à la chasse au Coq (démonstration)

 Valentin Blot , Louise Dubois de Prisque , Chantal Keller , Pierre Vial
JFLA 2022 - Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France
Communication dans un congrès hal-03604902v1
Image document

Compositional pre-processing for automated reasoning in dependent type theory

 Valentin Blot , Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , et al.
CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
Communication dans un congrès hal-03901019v3
Image document

Dependent Types and Multi-Monadic Effects in F*

 Nikhil Swamy , Cătălin Hriţcu , Chantal Keller , Aseem Rastogi , Antoine Delignat-Lavaud , et al.
43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016, St. Petersburg, Florida, United States. pp.256-270, ⟨10.1145/2837614.2837655⟩
Communication dans un congrès hal-01265793v1
Image document

On the Semantics of Polychronous Polytimed Specifications

 Hai Nguyen Van , Thibaut Balabonski , Frédéric Boulanger , Chantal Keller , Benoît Valiron , et al.
18th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2020, Vienna, Austria. pp.23-40, ⟨10.1007/978-3-030-57628-8_2⟩
Communication dans un congrès hal-02931403v1
Image document

Extended Resolution as Certificates for Propositional Logic

 Chantal Keller
PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States
Communication dans un congrès hal-00836845v1
Image document

Typeful Normalization by Evaluation

 Olivier Danvy , Chantal Keller , Matthias Puech
20th International Conference on Types for Proofs and Programs, TYPES 2014, May 2014, Paris, France. ⟨10.4230/LIPIcs.xxx.yyy.p⟩
Communication dans un congrès hal-01397929v1
Image document

Des transformations logiques passent leur certificat

 Quentin Garchery , Chantal Keller , Claude Marché , Andrei Paskevich
JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
Communication dans un congrès hal-02384946v2
Image document

A Coq formalisation of SQL's execution engines

 Véronique Benzaken , Évelyne Contejean , Chantal Keller , Eunice Martins
ITP 2018 - International Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.88-107, ⟨10.1007/978-3-319-94821-8_6⟩
Communication dans un congrès hal-01716048v1
Image document

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

 Mickaël Armand , Germain Faure , Benjamin Grégoire , Chantal Keller , Laurent Théry , et al.
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland
Communication dans un congrès inria-00614041v1
Image document

The Refined Calculus of Inductive Construction: Parametricity and Abstraction

 Chantal Keller , Marc Lasson
LICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnik, Croatia
Communication dans un congrès hal-00757620v1
Image document

Importing HOL Light into Coq

 Chantal Keller , Benjamin Werner
ITP - Interactive Theorem Proving, First International Conference - 2010, Jul 2010, Edimbourg, United Kingdom. pp.307-322
Communication dans un congrès inria-00520604v1
Image document

Tactic Program-based Testing and Bounded Verification in Isabelle/HOL

 Chantal Keller
Tests and Proofs, Jun 2018, Toulouse, France
Communication dans un congrès hal-01884960v1
Image document

PxTP 2021 - Seventh Workshop on Proof eXchange for Theorem Proving

 Chantal Keller , Mathias Fleury
Electronic Proceedings in Theoretical Computer Science, 336, 61 p., 2021, ⟨10.4204/eptcs.336⟩
N°spécial de revue/special issue hal-03443742v1
Image document

33èmes journées francophones des langages applicatifs

 Chantal Keller , Timothy Bourke , Sandrine Blazy , Frédéric Bour , Guillaume Bury , et al.
Chantal Keller; Timothy Bourke. , pp.1-292, 2022
Ouvrages hal-03689075v1
Image document

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

 Michaël Armand , Germain Faure , Benjamin Grégoire , Chantal Keller , Laurent Thery , et al.
CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩
Communication dans un congrès istex hal-00639130v1
Image document

A Certified Compiler for Verifiable Computing

 Cédric Fournet , Chantal Keller , Vincent Laporte
IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal
Communication dans un congrès hal-01397680v1
Image document

Translating canonical SQL to imperative code in Coq

 Véronique Benzaken , Évelyne Contejean , Mohammed Houssem Hachmaoui , Chantal Keller , Louis Mandel , et al.
Proceedings of the ACM on Programming Languages, 2022, 6 (OOPSLA1), pp.1-27. ⟨10.1145/3527327⟩
Article dans une revue hal-03876233v1
Image document

A Matter of Trust: Skeptical Communication Between Coq and External Provers

 Chantal Keller
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. ⟨NNT : ⟩
Thèse pastel-00838322v1
Image document

Vers une formalisation en Coq de la provenance de données

 Véronique Benzaken , Sarah Cohen-Boulakia , Évelyne Contejean , Chantal Keller , Rébecca Zucchini
31ème Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. pp.72-87
Communication dans un congrès hal-03080066v1
Image document

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

 Burak Ekici , Guy Katz , Chantal Keller , Alain Mebsout , Andrew J Reynolds , et al.
Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016, Jul 2016, Coimbra, Portugal
Communication dans un congrès hal-01388984v1
Image document

A Symbolic Operational Semantics for TESL with an Application to Heterogeneous System Testing

 Hai Nguyen Van , Thibaut Balabonski , Frédéric Boulanger , Chantal Keller , Benoît Valiron , et al.
15th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS 2017, Sep 2017, Berlin, Germany. ⟨10.1007/978-3-319-65765-3_18⟩
Communication dans un congrès hal-01583815v1
Image document

SMTCoq: automatisation expressive et extensible dans Coq

 Valentin Blot , Amina Bousalem , Quentin Garchery , Chantal Keller
JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
Communication dans un congrès hal-02369249v1
Page :