 |
 |
 |
 |
|
|
||
|---|---|---|
|
hal-00787126v2
Communication dans un congrès
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur. Reasoning About Higher-Order Relational Specifications Tom Schrijvers. International Symposium on Principles and Practice of Declarative Programming, Sep 2013, Madrid, Spain. ACM, 2013, <10.1145/2505879.2505889> |
||
|
inria-00201085v1
Communication dans un congrès
Axelle Ziegler, Dale Miller, Catuscia Palamidessi. A Congruence Format for Name-passing Calculi Peter Mosses and Irek Ulidowski. 2nd Workshop on Structural Operational Semantics (SOS'05), Jul 2005, Lisboa, Portugal. Elsevier, 156 (1), pp.169-189, 2006, Electronic Notes in Theoretical Computer Science; Proceedings of the 2nd Workshop on Structural Operational Semantics. <10.1016/j.entcs.2005.09.032> |
||
|
hal-00906485v1
Communication dans un congrès
Zakaria Chihani, Dale Miller, Fabien Renaud. Foundational proof certificates in first-order logic CADE - 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, United States. 2013 |
||
|
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-01424749v1
Communication dans un congrès
Tomer Libal, Alexander Steen. Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers 5th Workshop on Practical Aspects of Automated Reasoning, Jul 2016, Coimbra, Portugal. 2016, Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning 2016), Coimbra, Portugal, July 2nd, 2016 |
||
|
hal-00770678v1
Communication dans un congrès
Lutz Straßburger. Cut Elimination in Nested Sequents for Intuitionistic Modal Logics Frank Pfenning. FoSSaCS 2013, Mar 2013, Rome, Italy. Springer, 7794, pp.209-224, 2013, LNCS; Foundations of Software Science and Computation Structures, 16th International Conference (FOSSACS). <10.1007/978-3-642-37075-5_14> |
||
|
hal-01425465v1
Communication dans un congrès
Beniamino Accattoli, Giulio Guerrieri. Open Call-by-Value 14th Asian Symposium on Programming Languages and Systems (APLAS), Nov 2016, Hanoi, Vietnam. pp.206 - 226, 2016, <http://soict.hust.edu.vn/~aplas2016/>. <10.1007/978-3-319-47958-3_12> |
||
|
tel-00772590v1
HDR
Lutz Straßburger. Towards a Theory of Proofs of Classical Logic Logic in Computer Science [cs.LO]. Université Paris-Diderot - Paris VII, 2011 |
||
|
hal-00772592v1
Communication dans un congrès
David Baelde, Dale Miller, Zachary Snow. Focused Inductive Theorem Proving IJCAR 2010 - International Joint Conference on Automated Deduction, 2010, Edinburgh, United Kingdom. 2010 |
||
|
hal-00772722v1
Communication dans un congrès
Dale Miller. A proposal for broad spectrum proof certificates CPP 2011 - First International Conference on Certified Proofs and Programs, 2011, Kenting, Taiwan. 2011 |
||
|
hal-00772727v1
Pré-publication, Document de travail
Dale Miller. Communicating and trusting proofs: The case for foundational proof certificates To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science.. 2013 |
||
|
hal-00772599v1
Communication dans un congrès
Dale Miller. Reasoning about computations using two-levels of logic APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, 2010, Shanghai, China. 2010 |
||
|
hal-00772606v1
Article dans une revue
Gacek Andrew, Dale Miller, Gopalan Nadathur. Nominal Abstraction Journal of Information and Computation, Elsevier, 2011, 209 (1), pp.48-73 |
||
|
hal-00527881v1
Communication dans un congrès
Alexis Saurin, Dale Miller. A game semantics for proof search, preliminary results Twenty-first Conference on the Mathematical Foundations of Programming Semantics - MFPS XXI, May 2005, Birmingham, United Kingdom. 155, pp.543-563, 2006, <10.1016/j.entcs.2005.11.072> |
||
|
hal-00527893v1
Communication dans un congrès
Alexis Saurin, Kaustuv Chaudhuri, Dale Miller. Canonical Sequent Proofs via Multi-Focusing Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, Sep 2008, Milano, Italy. pp.383-396, 2008, <10.1007/978-0-387-09680-3_26> |
||
|
hal-00527888v1
Communication dans un congrès
Alexis Saurin, Dale Miller. From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic 16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Sep 2007, Lausanne, Switzerland. Springer, pp.405-419, 2007, Lecture notes in computer science. <10.1007/978-3-540-74915-8_31> |
||
|
hal-00527897v1
Communication dans un congrès
Alexis Saurin. Towards Ludics Programming: Interactive Proof Search 24th International Conference on Logic Programming - ICLP 2008, Dec 2008, Udine, Italy. Springer, pp.253-268, 2008, Lecture notes in computer science. <10.1007/978-3-540-89982-2_27> |
||
|
hal-01379683v1
Communication dans un congrès
Tomer Libal, Dale Miller. Functions-as-constructors Higher-order Unification 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Jun 2016, Porto, Portugal. Leibniz International Proceedings in Informatics (LIPIcs), pp.1 - 17, 2016, <10.4230/LIPIcs.FSCD.2016.26> |
||
|
hal-01379625v1
Communication dans un congrès
Tomer Libal, Marco Volpe. Certification of Prefixed Tableau Proofs for Modal Logic the Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2016), Sep 2016, Catania, Italy. Proceedings GandALF 2016, 226, pp.257 - 271, 2016, <10.4204/EPTCS.226.18> |
||
|
hal-01379624v1
Communication dans un congrès
Sonia Marin, Dale Miller, Marco Volpe. A focused framework for emulating modal proof systems Lev Beklemishev; Stéphane Demri; András Máté. 11th conference on "Advances in Modal Logic", Aug 2016, Budapest, Hungary. College Publications, pp.469-488, Advances in Modal Logic |
||
|
hal-00780774v2
Communication dans un congrès
Ivan Gazeau, Dale Miller, Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics Luca Bortolussi and Herbert Wiklicky. QAPL - 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, Mar 2013, Rome, Italy. Open Publishing Association, 117, pp.1-18, 2013, Electronic Proceedings in Theoretical Computer Science; Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL). <10.4204/EPTCS.117.1> |
||
|
hal-00759215v1
Article dans une revue
Lutz Straßburger. Extension without Cut Ann. Pure Appl. Logic, Elsevier, 2012, 163 (12), pp.1995-2007. <10.1016/j.apal.2012.07.004> |
||
|
hal-00759228v1
Communication dans un congrès
Stefan Hetzl, Lutz Straßburger. Herbrand-Confluence for Cut Elimination in Classical First Order Logic CSL 2012, Sep 2012, Fontainebleau, France. 2012, <http://drops.dagstuhl.de/opus/volltexte/2012/3681/>. <10.4230/LIPIcs.CSL.2012.320> |
||
|
hal-01425560v1
Communication dans un congrès
Beniamino Accattoli. The Complexity of Abstract Machines Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), Jun 2016, Porto, Portugal. 235, pp.1 - 15, 2017, <https://project.inria.fr/wpte2016/>. <10.4204/EPTCS.235.1> |
||
|
hal-01426753v1
Communication dans un congrès
Taus Brock-Nannestad. Space-efficient Planar Acyclicity Constraints - A Declarative Pearl FLOPS 2016 - 13th International Symposium on Functional and Logic Programming, Mar 2016, Kochi, Japan |
||
|
hal-00772347v1
Communication dans un congrès
Liang Chuck, Dale Miller. A Unified Sequent Calculus for Focused Proofs LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States. 2009 |
||
|
hal-00772332v1
Communication dans un congrès
Nigam Vivek, Dale Miller. Algorithmic specifications in linear logic with subexponentials PPDP09 - ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Sep 2009, Coimbra, Portugal. 2009 |
||
|
hal-01425534v1
Communication dans un congrès
Beniamino Accattoli. The Useful MAM, a Reasonable Implementation of the Strong $\lambda$-Calculus 23rd International Workshop on Logic, Language, Information, and Computation (WoLLIC 2016), Aug 2016, Puebla, Mexico. pp.1 - 21, 2016, <http://www.wollic.cs.buap.mx/>. <10.1007/978-3-662-52921-8_1> |
||
|
hal-00772420v1
Communication dans un congrès
Kaustuv Chaudhuri, Nicolas Guenot, Lutz Straßburger. The Focused Calculus of Structures Marc Bezem. 20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. 12, pp.159-173, 2011, Leibniz International Proceedings in Informatics (LIPIcs). <10.4230/LIPIcs.CSL.2011.159> |
||
|
hal-00772396v1
Communication dans un congrès
Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus Patrick Cégielski and Arnaud Durand. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. 16, pp.183-197, 2012, Leibniz International Proceedings in Informatics (LIPIcs). <10.4230/LIPIcs.CSL.2012.183> |
||
|
|
||