18 résultats  enregistrer la recherche


...
hal-00906789v1  Communication dans un congrès
Stéphane Graham-LengrandPsyche: 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 BernadetStéphane Graham-LengrandFilter 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 BernadetStéphane Graham-LengrandComplexity 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-LengrandSlot 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 FarooqueStéphane Graham-LengrandAssia MahboubiA 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-01242866v1  Communication dans un congrès
Stéphane Graham-LengrandRealisability 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 BonacinaStéphane Graham-LengrandNatarajan ShankarA 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 RouhlingMahfuza FarooqueStéphane Graham-LengrandJean-Marc NotinAssia MahboubiAxiomatic 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 BernadetStéphane Graham-LengrandA simple presentation of the effective topos
[Research Report] LIX, Ecole polytechnique. 2012
...
hal-00906778v1  Article dans une revue
Alexis BernadetStéphane Graham-LengrandNon-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-LengrandRoy DyckhoffJames MckinnaA 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>