Filtrer vos résultats
- 16
- 11
- 15
- 4
- 4
- 2
- 1
- 1
- 2
- 1
- 27
- 1
- 1
- 1
- 1
- 2
- 2
- 1
- 1
- 2
- 2
- 2
- 2
- 1
- 2
- 2
- 2
- 1
- 1
- 24
- 3
- 18
- 11
- 6
- 3
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 27
- 10
- 7
- 4
- 4
- 3
- 3
- 3
- 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
27 résultats
|
|
triés par
|
A Coq Formalization of the Relational Data ModelESOP - 23rd European Symposium on Programming, Apr 2014, Grenoble, France
Communication dans un congrès
hal-00924156v1
|
|||
|
Ground Associative and Commutative Completion Modulo Shostak TheoriesLPAR, Oct 2010, Yogyakarta, Indonesia
Communication dans un congrès
inria-00535652v1
|
||
Certification of automated termination proofs[Research Report] CEDRIC-07-1185, CEDRIC Lab/CNAM. 2007
Rapport
hal-01125298v1
|
|||
Mechanically proving termination using polynomial interpretations[Intern report] 1382, 2006
Rapport
inria-00001167v1
|
|||
|
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.67-81, ⟨10.1007/978-3-642-31365-3_8⟩
Communication dans un congrès
hal-00687640v2
|
||
|
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
|
||
Certification of automated termination proofs6th Int. Symp. on Frontiers of Combining Systems, Liverpool, Royaume-Uni, Jan 2007, X, France. pp.148-162
Communication dans un congrès
hal-01125312v1
|
|||
|
Complete Solving of Linear Diophantine Equational and Inequational Systems without Adding Variables[Technical Report] RT-0175, INRIA. 1995, pp.23
Rapport
inria-00069996v1
|
||
|
Canonized Rewriting and Ground AC Completion Modulo Shostak TheoriesTACAS - Tools and Algorithms for the Construction and Analysis of Systems, 2011, Saarbrücken, Germany
Communication dans un congrès
hal-00777663v1
|
||
|
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and ImplementationLogical Methods in Computer Science, 2012, 8 (3:16), pp.1-29. ⟨10.2168/LMCS-8(3:16)2012⟩
Article dans une revue
hal-00798082v1
|
||
|
Certifying Standard and Stratified Datalog Inference Engines in SSReflectInternational Conference on Interective Theorem Proving, 2017, Brasilia, Brazil
Communication dans un congrès
hal-01745566v1
|
||
|
Facettes de la preuveLogique en informatique [cs.LO]. Université Paris-Sud, 2014
HDR
tel-01089490v1
|
||
|
SQL à l'épreuve de Coq Une sémantique formelle pour SQLJournées Francophones des Langages Applicatifs (JFLA), Jan 2019, Les Rousses, France
Communication dans un congrès
hal-01952023v1
|
||
Deep-Embedded Unification[Research Report] CEDRIC-08-1547, CEDRIC Lab/CNAM. 2008
Rapport
hal-01125541v1
|
|||
Reflecting Proofs in First-Order Logic with Equality20th International Conference on Automated Deduction (CADE-20), 2005, Tallinn, Estonia. pp.7--22, ⟨10.1007/11532231_2⟩
Communication dans un congrès
istex
hal-00946061v1
|
|||
Cantor : On Ordinal Notations2006
Autre publication scientifique
hal-00344337v1
|
|||
Introducing Global Constraints in CHIPMathl. Comput. Modelling, 1994, 20 (12), pp.97--123
Article dans une revue
hal-00442810v1
|
|||
|
A Coq mechanised formal semantics for realistic SQL queries * Formally reconciling SQL and bag relational algebra2018
Pré-publication, Document de travail
hal-01830255v2
|
||
|
A Coq formalization of data provenanceCertified Programs and Proofs, ACM, Jan 2021, Virtual Event, Denmark. ⟨10.1145/3437992.3439920⟩
Communication dans un congrès
hal-03380459v1
|
||
|
SQLCert: Coq mechanisation of SQL's compilation: Formally reconciling SQL and (relational) algebra2016
Pré-publication, Document de travail
hal-01487062v1
|
||
|
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
|
||
|
Formal proofs applied to system modelsJFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.121-133
Communication dans un congrès
hal-03936894v2
|
||
|
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
|
||
Automated Certified Proofs with CiME3RTA - 22nd International Conference on Rewriting Techniques and Applications, 2011, Novi Sad, Serbia
Communication dans un congrès
hal-00777669v1
|
|||
Mechanically Proving Termination Using Polynomial InterpretationsJournal of Automated Reasoning, 2005, 34 (4), pp.325-363. ⟨10.1007/s10817-005-9022-x⟩
Article dans une revue
istex
hal-01984434v1
|
|||
|
A3PAT, an Approach for Certified Automated Termination Proofs2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, ACM, Jan 2010, Madrid, Spain. pp.63-72, ⟨10.1145/1706356.1706370⟩
Communication dans un congrès
inria-00535655v1
|
||
|
A Coq Mechanised Formal Semantics for Realistic SQL QueriesCPP 19, ACM, Jan 2019, Cascais, Portugal. pp.249-261, ⟨10.1145/3293880.3294107⟩
Communication dans un congrès
hal-01955433v1
|