Filtrer vos résultats
- 196
- 22
- 95
- 47
- 29
- 13
- 13
- 7
- 5
- 4
- 3
- 1
- 1
- 1
- 1
- 212
- 22
- 9
- 4
- 1
- 21
- 8
- 18
- 14
- 12
- 17
- 19
- 15
- 15
- 16
- 26
- 13
- 27
- 11
- 2
- 1
- 1
- 2
- 1
- 189
- 29
- 147
- 77
- 71
- 59
- 23
- 22
- 19
- 12
- 8
- 7
- 7
- 7
- 7
- 7
- 7
- 7
- 6
- 6
- 6
- 5
- 5
- 5
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 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
- 36
- 29
- 16
- 14
- 13
- 11
- 11
- 10
- 9
- 9
- 9
- 8
- 7
- 7
- 6
- 6
- 6
- 6
- 6
- 6
- 5
- 5
- 5
- 5
- 4
- 4
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 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
218 résultats
|
Model Checking and Theorem ProvingComputation and Language [cs.CL]. Paris Diderot, 2015. English. ⟨NNT : ⟩
Thèse
tel-01251073v1
|
||
|
SizeChangeTool: A Termination Checker for Rewriting Dependent TypesHOR 2019 - 10th International Workshop on Higher-Order Rewriting, Jun 2019, Dortmund, Germany. pp.14-19
Communication dans un congrès
hal-02442465v1
|
||
|
mSAT:An OCaml SAT SolverOCaml Users and Developers Workshop, Sep 2017, Oxford, United Kingdom
Poster de conférence
hal-01670765v1
|
||
|
Models and termination of proof reduction in the λΠ-calculus modulo theory2017
Pré-publication, Document de travail
hal-01101834v2
|
||
|
Adequate and Computational Encodings in the Logical Framework DeduktiFSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.25⟩
Communication dans un congrès
hal-03956666v1
|
||
|
Execution traces and reduction sequences2018
Pré-publication, Document de travail
hal-04060154v1
|
||
|
Importer les preuves de Logipedia dans AgdaThéorie et langage formel [cs.FL]. 2020
Mémoire d'étudiant
hal-02985530v1
|
||
|
Two linearities for quantum computing in the lambda calculusBioSystems, 2019
Article dans une revue
hal-02909128v1
|
||
|
The Physical Church-Turing Thesis and the Principles of Quantum TheoryInternational Journal of Foundations of Computer Science, 2012, 23 (5), pp.1131-1146. ⟨10.1142/S0129054112500153⟩
Article dans une revue
hal-00944482v1
|
||
|
The physical Church-Turing thesis and the principles of quantum theoryQIPC, 2011, Zurich, Switzerland. Local proceedings
Communication dans un congrès
hal-00944544v1
|
||
|
Traduction de HOL en DeduktiLogique en informatique [cs.LO]. 2012
Mémoire d'étudiant
hal-00919871v1
|
||
|
Logtk : A Logic ToolKit for Automated Reasoning and its Implementation4th Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienna, Austria
Communication dans un congrès
hal-01101057v1
|
||
|
On the definition of the classical connectives and quantifiers2013
Pré-publication, Document de travail
hal-00919437v1
|
||
|
A Logical Approach to CTL2014
Pré-publication, Document de travail
hal-00919467v1
|
||
|
Quantum CNOT Circuits Synthesis for NISQ Architectures Using the Syndrome Decoding ProblemReversible Computation, Jul 2020, Oslo, Norway. ⟨10.1007/978-3-030-52482-1_11⟩
Communication dans un congrès
hal-04349410v1
|
||
|
Confluence of left-linear higher-order rewrite theories by checking their nested critical pairsMathematical Structures in Computer Science, 2022, pp.1-36. ⟨10.1017/S0960129522000044⟩
Article dans une revue
hal-03126111v3
|
||
|
Generic bidirectional typing for dependent type theories2023
Pré-publication, Document de travail
hal-04270368v1
|
||
|
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq2023
Pré-publication, Document de travail
hal-04077552v1
|
||
|
A constructive proof of Skolem theorem for constructive logic2005
Pré-publication, Document de travail
hal-04099179v1
|
||
|
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus ModuloPxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. pp.43-57
Communication dans un congrès
hal-00921513v1
|
||
|
Automata, Resolution, and Cut-elimination2016
Pré-publication, Document de travail
hal-04063102v2
|
||
|
Using Event-Based Style for Developing M2M ApplicationsGPC - 8th International Conference on Grid and Pervasive Computing - 2013, 2013, Seoul, South Korea. pp.348-357, ⟨10.1007/978-3-642-38027-3_37⟩
Communication dans un congrès
hal-00924491v1
|
||
Toward the Rational Design of Galactosylated Glycoclusters That Target Pseudomonas aeruginosa Lectin A (LecA): Influence of Linker Arms That Lead to Low-Nanomolar Multivalent LigandsChemistry - A European Journal, 2016, 22 (33), pp.11785-11794. ⟨10.1002/chem.201602047⟩
Article dans une revue
istex
hal-02116180v1
|
|||
|
Encoding Proofs in Dedukti: the case of Coq proofsProceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal
Communication dans un congrès
hal-01330980v1
|
||
|
The New Rewriting Engine of DeduktiFSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.16, ⟨10.4230/LIPIcs.FSCD.2020.35⟩
Communication dans un congrès
hal-02981561v2
|
||
|
A Lightweight Double-negation TranslationLPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji
Communication dans un congrès
hal-01245021v1
|
||
|
Quantum Multiple-Valued Decision Diagrams in Graphical CalculiMFCS 2021 - 46th International Symposium on Mathematical Foundations of Computer Science, Aug 2021, Tallinn, Estonia. pp.89:1--89:15, ⟨10.4230/LIPIcs.MFCS.2021.89⟩
Communication dans un congrès
hal-03277262v1
|
||
|
Quantum causal graph dynamicsPhysical Review D, 2017, 96 (2), pp.024026
Article dans une revue
hal-01785461v1
|
||
|
Algorithmes et modèles : l'histoire d'une convergence2012
Pré-publication, Document de travail
hal-04061691v1
|
||
|
Cut-elimination and the decidability of reachability in alternating pushdown systems2015
Pré-publication, Document de travail
hal-01101835v1
|