This list has been generated on 1 July 2024 from HAL and may be outdated.
You can check out our latest list of publications on HAL.
Showing 220 articles.
Translating HOL-Light proofs to Coq
Frédéric Blanqui
LPAR-25 - 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2024)
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
FoSSaCS 2024 - 27th International Conference on Foundations of Software Science and Computation Structures (2024)
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
(2024)
Towards Formalization and Sharing of Atelier B Proofs with Dedukti
Claude Stolze, Olivier Hermant, Romain Guillaumé
(2024)
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, Bas Spitters
CPP 2024 - 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (2024)
Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti
Thiago Felicissimo, Théo Winterhalter
(2024)
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Ștefan Ciobâcă, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter
Proceedings of the ACM on Programming Languages (2024)
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
Philipp Haselwarter, Exequiel Rivas, Antoine van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cătălin Hriţcu, Kenji Maillard, Bas Spitters
ACM Transactions on Programming Languages and Systems (TOPLAS) (2023)
A semantics of K into dedukti, Une sémantique de K en dedukti
Amélie Ledein, Valentin Blot, Catherine Dubois
TYPES 2022 - 28th International Conference on Types for Proofs and Programs (TYPES) (2023)
Diller-Nahm Bar Recursion
Valentin Blot
FSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction (2023)
The Rewster: The Coq Proof Assistant with Rewrite Rules
Gaëtan Gilbert, Yann Leray, Nicolas Tabareau, Théo Winterhalter
TYPES 2023 - 29th International Conference on Types for Proofs and Programs (2023)
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq
Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
(2023)
A modular construction of type theories
Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, François Thiré
Logical Methods in Computer Science (2023)
Unification of Drags and Confluence of Drag Rewriting
Jean-Pierre Jouannaud, Fernando Orejas
Journal of Logical and Algebraic Methods in Programming (2023)
Traduire l'univers des mathématiques en Dedukti, sans univers
Amélie Ledein, Elliot Butte
JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs (2023)
Recommandations sur les « éditeurs de la zone grise »
Frédéric Blanqui, Anne Canteaut, Hidde de Jong, Sébastien Imperiale, Nathalie Mitton, Guillaume Pallez, Xavier Pennec, Xavier Rival, Bertrand Thirion
(2023)
Compositional pre-processing for automated reasoning in dependent type theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
CPP 2023 - Certified Programs and Proofs (2023)
Translating proofs from an impredicative type system to a predicative one
Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal
31st EACSL Annual Conference on Computer Science Logic (CSL 2023) (2023)
A New Connective in Natural Deduction, and its Application to Quantum Computing
Alejandro Díaz-Caro, Gilles Dowek
Theoretical Computer Science (2023)
Explanation: from ethics to logic
Gilles Dowek
Annals of the Japan Association for Philosophy of Science (2023)
Expressing predicate subtyping in computational logical frameworks, Expression du sous-typage par prédicats dans les cadres logiques calculatoires
Gabriel Hondet
(2022)
From the Universality of Mathematical Truth to the Interoperability of Proof Systems
Gilles Dowek
IJCAR 2022 - International Joint Conference on Automated Reasoning (2022)
Adequate and Computational Encodings in the Logical Framework Dedukti
Thiago Felicissimo
FSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction (2022)
Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity
Frédéric Blanqui
FSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction (2022)
Linear Lambda-Calculus is Linear
Alejandro Díaz-Caro, Gilles Dowek
FSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction (2022)
A direct computational interpretation of second-order arithmetic via update recursion
Valentin Blot
LICS 2022 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science (2022)
An Implementation of Set Theory with Pointed Graphs in Dedukti
Valentin Blot, Gilles Dowek, Thomas Traversié
LFMTP 2022 - International Workshop on Logical Frameworks and Meta-Languages : Theory and Practice (2022)
Classical simulation of quantum circuits with partial and graphical stabiliser decompositions
Aleks Kissinger, Renaud Vilmart, John van de Wetering
17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022) (2022)
Vers une traduction de K en Dedukti
Amélie Ledein, Valentin Blot, Catherine Dubois
JFLA 2022 - Journées Francophones des Langages Applicatifs (JFLA) (2023)
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 (2022)
LibNDT: towards a formal library on spreadable properties over linked nested datatypes
Mathieu Montin, Amélie Ledein, Catherine Dubois
Ninth Workshop on Mathematically Structured Functional Programming (MSFP) (2022)
A New Connective in Natural Deduction, and its Application to Quantum Computing
Alejandro Díaz-Caro, Gilles Dowek
(2022)
Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu
Mathematical Structures in Computer Science (2022)
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
Michael Färber
11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CCP'22) (2022)
M1 Internship Report Translating proofs between Isabelle and Dedukti, Rapport de stage M1 Traduction de preuves entre Isabelle et Dedukti
Yann Leray
(2021)
Confluence in UnTyped Higher-Order Theories by means of Critical Pairs
Gaspard Férey, Jean-Pierre Jouannaud
(2021)
Integrating Automated Theorem Provers in Proof Assistants, Utiliser des démonstrateurs automatiques dans un assistant à la preuve
Yacine El Haddad
(2021)
Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories
Gaspard Férey, Jean-Pierre Jouannaud
PPDP 2021 - 23rd International Symposium on Principles and Practice of Declarative Programming (2021)
Quantum Multiple-Valued Decision Diagrams in Graphical Calculi
Renaud Vilmart
MFCS 2021 - 46th International Symposium on Mathematical Foundations of Computer Science (2021)
Some Axioms for Mathematics
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction (2021)
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 (2021)
Higher-Order Confluence and Universe Embedding in the Logical Framework, Confluence d'ordre supérieur et encodage d'univers dans le Logical Framework
Gaspard Ferey
(2021)
Geometry of Interaction for ZX-Diagrams
Kostia Chardonnet, Benoît Valiron, Renaud Vilmart
TLLA 2021 - 5th International Workshop on Trends in Linear Logic and Applications (2021)
Interacting Safely with an Unsafe Environment
Gilles Dowek
Logical Frameworks and Meta-Languages (2021)
Interoperability between proof systems using the logical framework Dedukti, Interopérabilité entre systèmes de preuves en utilisant le cadre logique Dedukti
François Thiré
(2020)
Importer les preuves de Logipedia dans Agda, Importing Logipedia proofs in Agda
Tristan Delort
(2020)
A calculus of expandable stores
Hugo Herbelin, Étienne Miquey
LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science (2020)
Quantum CNOT Circuits Synthesis for NISQ Architectures Using the Syndrome Decoding Problem
Timothée Goubault de Brugière, Marc Baboulin, Benoît Valiron, Simon Martiel, Cyril Allouche
Reversible Computation (2020)
Encoding Agda Programs Using Rewriting
Guillaume Genestier
FSCD - 5th International Conference on Formal Structures for Computation and Deduction (2020)
The New Rewriting Engine of Dedukti
Gabriel Hondet, Frédéric Blanqui
FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction (2020)
Type safety of rewrite rules in dependent types
Frédéric Blanqui
FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction (2020)
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory
Bruno Barras, Valentin Maestracci
LFMPT 2020 - Logical Frameworks and Meta-Languages: Theory and Practice 2020 (2020)
Linking focusing and resolution with selection
Guillaume Burel
ACM Transactions on Computational Logic (2020)
The Algebra of Infinite Sequences: Notations and Formalization
Nachum Dershowitz, Jean-Pierre Jouannaud, Qian Wang
(2020)
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory
Gabriel Hondet, Frédéric Blanqui
TYPES 2020 - 26th International Conference on Types for Proofs and Programs (2020)
Les réseaux condition nécessaire du confinement et nouvel outil de santé publique
Gilles Dowek
(2020)
Theoretical Computer Science: Computability, Decidability and Logic
Olivier Bournez, Gilles Dowek, Rémi Gilleron, Serge Grigorieff, Jean-Yves Marion, Simon Perdrix, S. Tison
(2020)
Theoretical Computer Science: Computational Complexity
Olivier Bournez, Gilles Dowek, Rémi Gilleron, Serge Grigorieff, Jean-Yves Marion, Simon Perdrix, S. Tison
(2020)
Confluence in (Un)Typed Higher-Order Theories by means of Critical Pairs
Gaspard Ferey, Jean-Pierre Jouannaud
(2019)
First-order automated reasoning with theories: when deduction modulo theory meets practice
Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant
Journal of Automated Reasoning (2019)
Checking the type safety of rewrite rules in the $\lambda\Pi$-calculus modulo rewriting
Jui-Hsuan Wu
(2019)
Efficient rewriting using decision trees, Réécriture efficace par arbres de décision
Gabriel Hondet
(2019)
Ekstrakto A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui
PxTP 2019 - Sixth Workshop on Proof eXchange for Theorem Proving (PxTP) (2019)
Drags: A Compositional Algebraic Framework for Graph Rewriting
Nachum Dershowitz, Jean-Pierre Jouannaud
Theoretical Computer Science (2019)
SizeChangeTool: A Termination Checker for Rewriting Dependent Types
Guillaume Genestier
HOR 2019 - 10th International Workshop on Higher-Order Rewriting (2019)
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction (2019)
Proof Normalisation in a Logic Identifying Isomorphic Propositions
Alejandro Díaz-Caro, Gilles Dowek
FSCD 2019 - International Conference on Formal Structures for Computation and Deduction (2019)
Cumulative Types Systems and Levels
François Thiré
LFMTP 2019 - Logical Frameworks and Meta-Languages: Theory and Practice (2019)
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
TYPES 2019 - 25th International Conference on Types for Proofs and Programs (2019)
Unboxing Mutually Recursive Type Definitions in OCaml
Simon Colin, Rodolphe Lepigre, Gabriel Scherer
JFLA 2019 - 30 èmes journées francophones des langages applicatifs (2019)
Two linearities for quantum computing in the lambda calculus
Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi
BioSystems (2019)
Towards Combining Model Checking and Proof Checking
Ying Jiang, Jian Liu, Gilles Dowek, Kailiang Ji
The Computer Journal (2019)
Graph Path Orderings
Nachum Dershowitz, Jean-Pierre Jouannaud
22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2018)
Industrial Placement Report Research Placement in Deducteam
Aristomenis-Dionysios Papadopoulos
(2018)
Linking focusing and resolution with selection
Guillaume Burel
43rd International Symposium on Mathematical Foundations of Computer Science(MFCS) (2018)
Termination of λΠ modulo rewriting using the size-change principle (work in progress)
Frédéric Blanqui, Guillaume Genestier
16th International Workshop on Termination (2018)
Drags: A Simple Algebraic Framework For Graph Rewriting
Nachum Dershowitz, Jean-Pierre Jouannaud
TERMGRAPH 2018 - 10th International Workshop on Computing with Terms and Graphs (2018)
Abstract Representation of Binders in OCaml using the Bindlib Library
Rodolphe Lepigre, Christophe Raffalli
Electronic Proceedings in Theoretical Computer Science (2018)
Sharing a Library between Proof Assistants: Reaching out to the HOL Family *
François Thiré
Electronic Proceedings in Theoretical Computer Science (2018)
Size-based termination of higher-order rewriting
Frédéric Blanqui
Journal of Functional Programming (2018)
Extending higher-order logic with predicate subtyping, Extension de la logique d'ordre supérieur avec le sous-typage par prédicats
Frédéric Gilbert
(2018)
Exporting an Arithmetic Library from Dedukti to HOL, Exporter une librairie d'arithmétique depuis Dedukti vers HOL
François Thiré
(2017)
Typing Quantum Superpositions and Measurement
Alejandro Díaz-Caro, Gilles Dowek
TPNC 2017 - 6th International Conference on the Theory and Practice of Natural Computing (2017)
Proof certificates in PVS
Frédéric Gilbert
ITP 2017 - 8th International Conference on Interactive Theorem Proving (2017)
Analyzing individual proofs as the basis of interoperability between proof systems
Gilles Dowek
PxTP 2017 - Fifth Workshop on Proof eXchange for Theorem Proving (2017)
Termination checking in the λΠ-calculus modulo theory. From a practical and a theoretical viewpoint, Vérification de la terminaison dans le λΠ-calcul modulo théorie. De la pratique à la théorie.
Guillaume Genestier
(2017)
PML 2 : Integrated Program Verification in ML
Rodolphe Lepigre
23rd International Conference on Types for Proofs and Programs (TYPES 2017) (2018)
Interoperability between arithmetic proofs using Dedukti, L'intéropérabilité entre des preuves d'arithmétique en utilisan Dedukti
Gilles Dowek, Stéphane Graham-Lengrand, François Thiré
International School On Rewriting 2017 (2017)
Coq without Type Casts: A Complete Proof of Coq Modulo Theory
Jean-Pierre Jouannaud, Pierre-Yves Strub
LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2017)
Untyped Confluence In Dependent Type Theories
Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
(2017)
Rules and derivations in an elementary logic course
Gilles Dowek
IfColog Journal of Logics and their Applications (FLAP) (2017)
Automated Deduction and Proof Certification for the B Method, Déduction Automatique et Certification de Preuve pour la Méthode B
Pierre Halmagrand
(2016)
Soundly Proving B Method Formulae Using Typed Sequent Calculus
Pierre Halmagrand
13th International Colloquium on Theoretical Aspects of Computing (ICTAC) (2016)
ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti
Raphaël Cauderlier, Catherine Dubois
ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing (2016)
Object-Oriented Mechanisms for Interoperability between Proof Systems, Mécanismes Orientés-Objets pour l'Interopérabilité entre Systèmes de Preuve
Raphaël Cauderlier
(2016)
Toward the Rational Design of Galactosylated Glycoclusters That Target Pseudomonas aeruginosa Lectin A (LecA): Influence of Linker Arms That Lead to Low-Nanomolar Multivalent Ligands
Shuai Wang, Lucie Dupin, Mathieu Noël, Cindy Carroux, Louis Renaud, Thomas Gehin, Albert Meyer, Eliane Souteyrand, Jean-Jacques Vasseur, Gérard Vergoten, Yann Chevolot, François Morvan, Sébastien Vidal
Chemistry - A European Journal (2016)
Resolution in Solving Graph Problems
Kailiang Ji
8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016) (2016)
Reversible Causal Graph Dynamics
Pablo Arrighi, Simon Martiel, Simon Perdrix
Reversible Computation (2016)
Encoding Proofs in Dedukti: the case of Coq proofs
Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
Proceedings Hammers for Type Theories (2016)
Untyped Confluence in Dependent Type Theories
Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
Proceedings Higher-Order Rewriting Workshop (2016)
A Rewrite System for Proof Constructivization
Raphaël Cauderlier
Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016 (2016)
Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system
Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
TYPES: Types for Proofs and Programs (2016)
Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval
Shuai Wang
AITP 2016 - Conference on Artificial Intelligence and Theorem Proving (2016)
Free fall and cellular automata
Pablo Arrighi, Gilles Dowek
Electronic Proceedings in Theoretical Computer Science (2016)
Discrete Geodesics and Cellular Automata
Pablo Arrighi, Gilles Dowek
Theory and Practice of Natural Computing (2015)
Termination of rewrite relations on λ-terms based on Girard's notion of reducibility
Frédéric Blanqui
Theoretical Computer Science (2015)
Normalization by Completeness with Heyting Algebras
Gaëtan Gilbert, Olivier Hermant
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2015)
A Lightweight Double-negation Translation
Frédéric Gilbert
LPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2015)
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2015)
Decidability, Introduction Rules and Automata
Gilles Dowek, Ying Jiang
International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (2015)
Implementing Polymorphism in Zenon
Guillaume Bury, Raphaël Cauderlier, Pierre Halmagrand
11th International Workshop on the Implementation of Logics (IWIL) (2015)
The Computability Path Ordering
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Logical Methods in Computer Science (2015)
Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable., An implicit Calculus of Constructions with dependent sums and decidable type inference.
Bruno Bernardo
(2015)
A framework for defining computational higher-order logics, Un cadre de définition de logiques calculatoires d’ordre supérieur
Ali Assaf
(2015)
Model Checking and Theorem Proving, Le model Checking et la émonstration de théorèmes
Kailiang Ji
(2015)
A Completion Method to Decide Reachability in Rewrite Systems
Guillaume Burel, Gilles Dowek, Ying Jiang
International Symposium on Frontiers of Combining Systems FroCoS'15 (2015)
Confluence of layered rewrite systems
Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
24th EACSL Annual Conference on Computer Science Logic (CSL 2015) (2015)
Translating HOL to Dedukti
Ali Assaf, Guillaume Burel
Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15 (2015)
Checking Zenon Modulo Proofs in Dedukti
Raphaël Cauderlier, Pierre Halmagrand
Fourth Workshop on Proof eXchange for Theorem Proving (PxTP) (2015)
Rewriting Modulo β in the λ Π-Calculus Modulo
Ronan Saillard
Logical Frameworks and Meta Languages: Theory and Practic, Affiliated with CADE-25 (2015)
Médiation en sciences du numériques : un levier pour comprendre notre quotidien ?
Sylvie Alayrangues, Gilles Dowek, Erwan Kerrien, Jean Mairesse, Thierry Viéville
Science & You (2015)
Cut-elimination and the decidability of reachability in alternating pushdown systems
Gilles Dowek, Ying Jiang
(2015)
Conservativity of embeddings in the lambda-Pi calculus modulo rewriting (long version)
Ali Assaf
(2015)
Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson, Benoît Valiron
Logical Methods in Computer Science (2014)
Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Simon Cruanes
4th Workshop on Practical Aspects of Automated Reasoning (2014)
Dedukti : un vérificateur de preuves universel
Ronan Saillard
Journées de seconde année de l'Ecole Doctorale à Mines ParisTech (2014)
Using Deduction Modulo in Set Theory
Pierre Halmagrand
SETS14, 1st International Workshop about Sets and Tools (2014)
A calculus of constructions with explicit subtyping
Ali Assaf
20th International Conference on Types for Proofs and Programs (TYPES 2014) (2015)
Objects and subtyping in the lambda-Pi-calculus modulo
Raphaël Cauderlier, Ali Assaf, Catherine Dubois
TYPES 2014 (2014)
Semantic A-translation and Super-consistency entail Classical Cut Elimination
Lisa Allali, Olivier Hermant
LPAR 19 - 19th Conference on Logic for Programming, Artificial Intelligence, and Reasoning - 2013 (2013)
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013 (2013)
Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
IWIL - 10th International Workshop on the Implementation of Logics - 2013 (2013)
Towards explicit rewrite rules in the λΠ-calculus modulo
Ronan Saillard
IWIL - 10th International Workshop on the Implementation of Logics (2013)
A Formal Proof of Square Root and Division Elimination in Embedded Programs
Pierre Neron
Journal of Formalized Reasoning (2013)
A Quest for Exactness: Program Transformation for Reliable Real Numbers, Transformation de Programmes pour des Nombres Réels Fiables
Pierre Neron
(2013)
Detection of First Order Axiomatic Theories
Guillaume Burel, Simon Cruanes
FroCoS - 9th International Symposium on Frontiers of Combining Systems - 2013 (2013)
Mining Malware Specifications through Static Reachability Analysis
Hugo Daniel Macedo, Tayssir Touili
ESORICS 2013 - 18th European Symposium on Research in Computer Security (2013)
The probability of non-confluent systems
Alejandro Díaz-Caro, Gilles Dowek
DCM - 9th International Workshop on Developments in Computational Models - 2013 (2014)
Informatique et sciences du numérique : Édition spéciale Python
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimellli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack, Hugues Bersini, Guillaume Le Blanc
(2013)
Square root and division elimination in PVS
Pierre Neron
ITP - 4th Conference on Interactive Theorem Proving (2013)
Real numbers, chaos, and the principle of a bounded density of information
Gilles Dowek
CSR 2013 - 8th International Computer Science Symposium in Russia (2013)
Programming Robots With Events
Truong Giang Le, Dmitriy Fedosov, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo
4th International Embedded Systems Symposium (IESS) (2013)
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo
Guillaume Burel
PxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013 (2013)
Dedukti:un vérificateur de preuves universel
Ali Assaf, Raphaël Cauderlier, Ronan Saillard
Journées nationales GDR - GPL - CIEL - AFADL (2013)
Médiation Scientifique : une facette de nos métiers de la recherche
Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas P. Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie de Quatrebarbes, Stéphane Laurent
(2013)
Call-by-value non-determinism in a linear logic type discipline
Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani
LFCS - Logical Foundations of Computer Science - 2013 (2013)
Universality in two dimensions
Nachum Dershowitz, Gilles Dowek
Journal of Logic and Computation (2013)
Using Event-Based Style for Developing M2M Applications
Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo
GPC - 8th International Conference on Grid and Pervasive Computing - 2013 (2013)
Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python
Judicaël Courant, Marc de Falco, Stéphane Gonnord, Jean-Christophe Filliâtre, Sylvain Conchon, Gilles Dowek, Benjamin Wack
(2013)
Typing linear algebra: A biproduct-oriented approach
Hugo Daniel Macedo, José N. Oliveira
Science of Computer Programming (2013)
Lineal: A linear-algebraic lambda-calculus
Pablo Arrighi, Gilles Dowek
Logical Methods in Computer Science (2013)
ML Dependency Analysis for Assessors
François Pessaux, Vincent Benayoun, Catherine Dubois, Philippe Ayrault
Software Engineering and Formal Methods (SEFM) 2012 (2012)
Non determinism through type isomorphism
Alejandro Díaz-Caro, Gilles Dowek
LSFA - 7th Workshop on Logical and Semantic Frameworks with Applications - 2012 (2013)
Informatique et Sciences du Numérique - Spécialité ISN en Terminale S
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimellli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack
(2012)
Informatique et sciences du numérique ― Spécialité ISN en terminale S, avec des exercices corrigés et des idées de projets
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimelli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack, Gérard Berry
(2012)
Causal Graph Dynamics
Pablo Arrighi, Gilles Dowek
ICALP 2012 - 39th International ColloquiumAutomata, Languages, and Programming (2012)
Tableaux Modulo Theories Using Superdeduction
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
IJCAR 2012 - 6th International Joint Conference on Automated Reasoning (2014)
The Physical Church-Turing Thesis and the Principles of Quantum Theory
Pablo Arrighi, Gilles Dowek
International Journal of Foundations of Computer Science (2012)
A simple proof that super consistency implies cut elimination
Gilles Dowek, Olivier Hermant
Notre Dame Journal of Formal Logic (2012)
Une introduction à la science informatique pour les enseignants de la discipline en lycée
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Sylvie Boldo, Denis Bouhineau, Patrick Cegielski, Thomas Heide Clausen, Irène Guessarian, Stéphane Lopes, Laurent Mounier, Benjamin Nguyen, Franck Quessette, Anne Rasse, Brigitte Rozoy, Claude Timsit, Thierry Viéville, Jean-Marc Vincent
(2011)
The physical Church-Turing thesis and the principles of quantum theory
Pablo Arrighi, Gilles Dowek
QIPC (2011)
Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View
Gilles Dowek
(2008)