Filtrer vos résultats
- 24
- 19
- 20
- 7
- 5
- 5
- 3
- 1
- 1
- 1
- 3
- 42
- 1
- 1
- 4
- 3
- 2
- 2
- 3
- 6
- 4
- 4
- 4
- 4
- 3
- 2
- 1
- 43
- 30
- 26
- 13
- 3
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 43
- 6
- 5
- 4
- 4
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
43 résultats
|
|
triés par
|
Special Issue on Computational Logic ( in honor to Roy Dyckhoff) of Journal of Logic and ComputationOxford University Press (OUP), 26 (2), 2016, ⟨10.1093/logcom/exu039⟩
Ouvrages
hal-01263202v1
|
|||
|
Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), Sep 2013, Nancy, France. pp.149--156
Communication dans un congrès
hal-00906789v1
|
||
A big-step operational semantics via non-idempotent intersection types[Research Report] LIX, Ecole polytechnique. 2013
Rapport
hal-01830232v1
|
|||
Special issue on computational logic in honour of Roy Dyckhoff. Journal of Logic and Computation.Oxford University Press, 2014, D M Gabbay
Ouvrages
hal-01094032v1
|
|||
Deriving strong normalisationHigher-Order Rewriting (HOR'04), Jun 2004, Aachen, Germany. pp.84 - 88
Communication dans un congrès
hal-00150289v1
|
|||
Call-by-value, call-by-name, and strong normalization for the classical sequent calculusNov 2003, pp.714-730
Communication dans un congrès
hal-00150290v1
|
|||
|
Filter models: non-idempotent intersection types, orthogonality and polymorphism - long version2011
Rapport
hal-00600070v3
|
||
|
An MCSAT treatment of Bit-Vectors (preliminary report)SMT 2017 - 15th International Workshop on Satisfiability Modulo Theories, Jul 2017, Heidelberg, Germany
Communication dans un congrès
hal-01615837v1
|
||
|
Normalisation & Equivalence in Proof Theory & Type TheoryMathematics [math]. Université Paris-Diderot - Paris VII; University of St Andrews, 2006. English. ⟨NNT : ⟩
Thèse
tel-00134646v1
|
||
Extending the Explicit Substitution ParadigmInternational Conference on Rewriting Techniques and Applications (RTA), 2005, Nara, Japan. pp.407-422
Communication dans un congrès
hal-00148847v1
|
|||
|
Complexity of strongly normalising λ-terms via non-idempotent intersection typesProceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'11), Sep 2011, Saarbruecken, Germany. pp.88-107, ⟨10.1007/978-3-642-19805-2_7⟩
Communication dans un congrès
hal-01110489v1
|
||
|
Proceedings of the Sixth Workshop on Intersection Types and Related Systems (ITRS'12)EPTCS, 121, pp.1--93, 2013, ⟨10.4204/EPTCS.121⟩
Ouvrages
hal-00912611v1
|
||
|
Tight typings and split bounds23rd ACM International Conference on Functional Programming, Sep 2018, St Louis, United States. pp.1 - 30, ⟨10.1145/3236789⟩
Communication dans un congrès
hal-01936141v1
|
||
Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logicInternational Joint Conference on Automated Reasoning (IJCAR), 2006, Seattle, United States. pp.347--361
Communication dans un congrès
hal-00148844v1
|
|||
|
Call-by-Value Lambda-calculus and LJQ2007
Pré-publication, Document de travail
hal-00150284v1
|
||
|
Polarities & Focussing: a journey from Realisability to Automated ReasoningLogic in Computer Science [cs.LO]. Paris-Sud XI, 2014
HDR
tel-01094980v1
|
||
|
A simple presentation of the effective topos[Research Report] LIX, Ecole polytechnique. 2012
Rapport
hal-00844250v1
|
||
|
Axiomatic constraint systems for proof search modulo theories10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Sep 2015, Wroclaw, Poland. ⟨10.1007/978-3-319-24246-0_14⟩
Communication dans un congrès
hal-01107944v1
|
||
Intersection types for explicit substitutionsInformation and Computation, 2004, 189 (1), pp.17 - 42
Article dans une revue
hal-00150285v1
|
|||
|
Classical F_omega, orthogonality and symmetric candidates2007
Pré-publication, Document de travail
hal-00150283v1
|
||
|
Realisability semantics of abstract focussing, formalisedProceedings of the First International Workshop on Focusing, Nov 2015, Suva, Fiji. pp.14, ⟨10.4204/EPTCS.197.3⟩
Communication dans un congrès
hal-01242866v1
|
||
|
Proofs in conflict-driven theory combinationProceedings of the 7th International Conference on Certified Programs and Proofs (CPP'18), Jan 2018, Los Angeles, United States. ⟨10.1145/3167096⟩
Communication dans un congrès
hal-01935595v1
|
||
|
Non-idempotent intersection types and strong normalisationLogical Methods in Computer Science, 2013, 9 (4), pp.17-42
Article dans une revue
hal-00906778v1
|
||
|
Two simulations about DPLL(T)2012
Rapport
hal-00690044v1
|
||
|
Satisfiability Modulo Theories and AssignmentsCADE 2017 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. ⟨10.1007/978-3-319-63046-5_4⟩
Communication dans un congrès
hal-01615830v1
|
||
Resource Operators for lambda-calculusInformation and Computation, 2007, 205 (4), pp.419-473
Article dans une revue
hal-00148539v1
|
|||
|
Induction principles as the foundation of the theory of normalisation: Concepts and Techniques2005
Pré-publication, Document de travail
hal-00004358v2
|
||
LJQ, a strongly Focused Calculus for Intuitionistic LogicComputability in Europe (CiE'06), Jun 2006, Swansea, United Kingdom. pp.173 - 185
Communication dans un congrès
hal-00150287v1
|
|||
Filter models: non-idempotent intersection types, orthogonality and polymorphismProceedings of the 20th Annual Conference of the European Association for Computer Science Logic (CSL'11), Sep 2011, Bergen, Norway. ⟨10.4230/LIPIcs.CSL.2011.51⟩
Communication dans un congrès
hal-01110486v1
|
|||
|
Termination of lambda-calculus with the extra Call-By-Value rule known as assoc.2007
Pré-publication, Document de travail
inria-00292029v2
|
- 1
- 2