|
|
||
|---|---|---|
|
hal-00906789v1
Communication dans un congrès
Stéphane Graham-Lengrand. Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture Didier Galmiche and Dominique Larchey-Wendling. 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), Sep 2013, Nancy, France. Springer-Verlag, 8123, pp.149--156, 2013, Lecture Notes in Computer Science |
||
|
hal-01110486v1
Communication dans un congrès
Alexis Bernadet, Stéphane Graham-Lengrand. Filter models: non-idempotent intersection types, orthogonality and polymorphism Marc Bezem. Proceedings of the 20th Annual Conference of the European Association for Computer Science Logic (CSL'11), Sep 2011, Bergen, Norway. Schloss Dagstuhl Leibniz Center for Informatics, 2011, Leibniz International Proceedings in Informatics. <10.4230/LIPIcs.CSL.2011.51> |
||
|
hal-01110489v1
Communication dans un congrès
Alexis Bernadet, Stéphane Graham-Lengrand. Complexity of strongly normalising λ-terms via non-idempotent intersection types Martin Hofmann. Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'11), Sep 2011, Saarbruecken, Germany. Springer-Verlag, 6604, pp.88-107, Lecture Notes in Computer Science. <10.1007/978-3-642-19805-2_7> |
||
|
hal-01211209v1
Communication dans un congrès
Stéphane Graham-Lengrand. Slot Machines: an approach to the Strategy Challenge in SMT solving (presentation only) 13th International Workshop on Satisfiability Modulo Theories, Jul 2015, San Francisco, United States |
||
|
hal-00854426v1
Communication dans un congrès
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus Alberto Momigliano and Brigitte Pientka and Randy Pollack. LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - 2013, Sep 2013, Boston, United States. ACM, 2013, <10.1145/2503887.2503892> |
||
|
hal-00912611v1
Ouvrage (y compris édition critique et traduction)
Stéphane Graham-Lengrand, Luca Paolini. Proceedings of the Sixth Workshop on Intersection Types and Related Systems (ITRS'12) EPTCS, 121, pp.1--93, 2013, <10.4204/EPTCS.121> |
||
|
hal-00690392v1
Pré-publication, Document de travail
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi. Simulating the DPLL(T ) procedure in a sequent calculus with focusing 2012 |
||
|
tel-01094980v1
HDR
Stéphane Graham-Lengrand. Polarities & Focussing: a journey from Realisability to Automated Reasoning Logic in Computer Science [cs.LO]. Paris-Sud XI, 2014 |
||
|
hal-01094032v1
Direction d'ouvrage, Proceedings
Didier Galmiche, Stéphane Graham-Lengrand. Special issue on computational logic in honour of Roy Dyckhoff. Journal of Logic and Computation. United Kingdom. Oxford University Press, 2014, <http://dx.doi.org/10.1093/logcom/exu039> |
||
|
hal-01242866v1
Communication dans un congrès
Stéphane Graham-Lengrand. Realisability semantics of abstract focussing, formalised Proceedings of the First International Workshop on Focusing, Nov 2015, Suva, Fiji. Electronic Proceedings in Theoretical Computer Science, 197, pp.14, 2015, <http://www.cs.cmu.edu/~wof15/>. <10.4204/EPTCS.197.3> |
||
|
hal-01425305v1
Rapport
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar. A model-constructing framework for theory combination [Research Report] RR-99/2016, Universita degli Studi di Verona. 2016 |
||
|
hal-01107944v1
Communication dans un congrès
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi. Axiomatic constraint systems for proof search modulo theories C. Lutz and S. Ranise. 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Sep 2015, Wroclaw, Poland. Springer, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), 9322, 2014, LNAI. <10.1007/978-3-319-24246-0_14> |
||
|
hal-00844250v1
Rapport
Alexis Bernadet, Stéphane Graham-Lengrand. A simple presentation of the effective topos [Research Report] LIX, Ecole polytechnique. 2012 |
||
|
hal-00906778v1
Article dans une revue
Alexis Bernadet, Stéphane Graham-Lengrand. Non-idempotent intersection types and strong normalisation Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (4), pp.17-42 |
||
|
hal-01110478v1
Article dans une revue
Stéphane Graham-Lengrand, Roy Dyckhoff, James Mckinna. A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2011, 7 (1), pp.33. <10.2168/LMCS-7(1:6)2011> |
||
|
|
||