Filtrer vos résultats
- 31
- 25
- 2
- 1
- 1
- 1
- 1
- 1
- 30
- 1
- 2
- 3
- 3
- 3
- 1
- 2
- 2
- 4
- 2
- 2
- 3
- 2
- 2
- 25
- 6
- 14
- 12
- 9
- 8
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 31
- 4
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
31 résultats
|
|
triés par
|
|
Beagle as a HOL4 external ATP methodPAAR - Fourth Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienne, Austria
Communication dans un congrès
hal-01089316v1
|
||
|
SMTCoq: A plug-in for integrating SMT solvers into CoqComputer Aided Verification - 29th International Conference, Jul 2017, Heidelberg, Germany
Communication dans un congrès
hal-01669345v1
|
||
|
General Automation in Coq through Modular TransformationsSeventh Workshop on Proof Exchange in Theorem Proving, Jul 2021, Pittsburgh, United States. ⟨10.4204/EPTCS.336.3⟩
Communication dans un congrès
hal-03328935v1
|
||
|
JFLA 2021 - 32 èmes Journées Francophones des Langages Applicatifs2021
Ouvrages
hal-03190426v2
|
||
|
Bécassine à la chasse au Coq (démonstration)JFLA 2022 - Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France
Communication dans un congrès
hal-03604902v1
|
||
|
Compositional pre-processing for automated reasoning in dependent type theoryCPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
Communication dans un congrès
hal-03901019v3
|
||
|
Dependent Types and Multi-Monadic Effects in F*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
|
||
|
On the Semantics of Polychronous Polytimed Specifications18th 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
|
||
|
Typeful Normalization by Evaluation20th 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
|
||
|
Extended Resolution as Certificates for Propositional LogicPxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States
Communication dans un congrès
hal-00836845v1
|
||
|
Des transformations logiques passent leur certificatJFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
Communication dans un congrès
hal-02384946v2
|
||
|
A Coq formalisation of SQL's execution enginesITP 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
|
||
|
Verifying SAT and SMT in Coq for a fully automated decision procedurePSATTT'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
|
||
|
The Refined Calculus of Inductive Construction: Parametricity and AbstractionLICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnik, Croatia
Communication dans un congrès
hal-00757620v1
|
||
|
Importing HOL Light into CoqITP - Interactive Theorem Proving, First International Conference - 2010, Jul 2010, Edimbourg, United Kingdom. pp.307-322
Communication dans un congrès
inria-00520604v1
|
||
|
HOL-TestGen Version 1.8 USER GUIDE[Technical Report] Univeristé Paris-Saclay; LRI - CNRS, University Paris-Sud. 2016
Rapport
hal-01765526v1
|
||
|
Parametricity in an Impredicative SortCSL - 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
|
||
|
Hereditary Substitutions for Simple Types, FormalizedMSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States
Communication dans un congrès
inria-00520606v1
|
||
|
An Interactive SMT Tactic in Coq using Abductive Reasoning24th 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
|
||
|
PxTP 2021 - Seventh Workshop on Proof eXchange for Theorem ProvingElectronic Proceedings in Theoretical Computer Science, 336, 61 p., 2021, ⟨10.4204/eptcs.336⟩
N°spécial de revue/special issue
hal-03443742v1
|
||
|
33èmes journées francophones des langages applicatifsOuvrages hal-03689075v1 |
||
|
A Modular Integration of SAT/SMT Solvers to Coq through Proof WitnessesCPP - 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
|
||
|
A Certified Compiler for Verifiable ComputingIEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal
Communication dans un congrès
hal-01397680v1
|
||
|
Tactic Program-based Testing and Bounded Verification in Isabelle/HOLTests and Proofs, Jun 2018, Toulouse, France
Communication dans un congrès
hal-01884960v1
|
||
|
Translating canonical SQL to imperative code in CoqProceedings of the ACM on Programming Languages, 2022, 6 (OOPSLA1), pp.1-27. ⟨10.1145/3527327⟩
Article dans une revue
hal-03876233v1
|
||
|
A Matter of Trust: Skeptical Communication Between Coq and External ProversLogic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. ⟨NNT : ⟩
Thèse
pastel-00838322v1
|
||
|
Pseudo-Weight: Making Tabletop Interaction with Virtual Objects More TangibleProceedings of the 2012 ACM international conference on Interactive Tabletops and Surfaces (ITS 2012), 2012, Cambridge, MA, United States. pp.201-204, ⟨10.1145/2396636.2451335⟩
Communication dans un congrès
hal-00953336v1
|
||
|
Vers une formalisation en Coq de la provenance de données31ème Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. pp.72-87
Communication dans un congrès
hal-03080066v1
|
||
|
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)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
|
||
|
A Symbolic Operational Semantics for TESL with an Application to Heterogeneous System Testing15th 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
|
- 1
- 2