| [1] | David Baelde. Logique linéaire et algèbre de processus. Technical report, INRIA Futurs, LIX and ENS, 2005. [ bib | .ps ] |
| [2] | David Baelde. A linear approach to the proof-theory of least and greatest fixed points. PhD thesis, Ecole Polytechnique, December 2008. [ bib | http ] |
| [3] | David Baelde. On the expressivity of minimal generic quantification. In A. Abel and C. Urban, editors, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), number 228 in ENTCS, pages 3-19, 2008. [ bib | http ] |
| [4] | David Baelde. On the proof theory of regular fixed points. In Martin Giese and Arild Waller, editors, TABLEAUX 09: Automated Reasoning with Analytic Tableaux and Related Methods, number 5607 in LNAI, pages 93-107, 2009. [ bib | .pdf ] |
| [5] | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. A User Guide to Bedwyr, November 2006. [ bib | .pdf ] |
| [6] | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The Bedwyr system for model checking over syntactic expressions. In F. Pfenning, editor, 21th Conf. on Automated Deduction (CADE), number 4603 in LNAI, pages 391-397, New York, 2007. Springer. [ bib | .pdf ] |
| [7] | David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In N. Dershowitz and A. Voronkov, editors, International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 4790 of LNCS, pages 92-106, 2007. [ bib | .pdf ] |
| [8] | David Baelde and Dale Miller. Least and greatest fixed points in linear logic: extended version. Technical report, available from the first author's web page, April 2007. [ bib | .pdf ] |
| [9] | David Baelde, Dale Miller, and Zachary Snow. Focused inductive theorem proving. In J. Giesl and R. Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, number 6173 in LNCS, pages 278-292, 2010. [ bib | .pdf ] |
| [10] | David Baelde and Samuel Mimram. De la webradio lambda à la λ-webradio. In Journées Francophones des Langages Applicatifs, pages 47-61. INRIA, 2008. [ bib | .pdf ] |
| [11] | Alexis Bernadet and Stéphane Lengrand. Complexity of strongly normalising λ-terms via non-idempotent intersection types. In Martin Hofmann, editor, Proceedings of the 14th international conference on Foundations of Software Science and Computation Structures (FOSSACS'11), volume 6604 of LNCS. Springer, March 2011. [ bib ] |
| [12] | Alexis Bernadet and Stéphane Lengrand. Filter models: non-idempotent intersection types, orthogonality and polymorphism. In Marc Bezem, editor, Proceedings of the 20th Annual conference of the European Association for Computer Science Logic (CSL'11), lipics. lci, September 2011. [ bib ] |
| [13] | Kai Brünnler and Lutz Straßburger. Modular sequent systems for modal logic. In Martin Giese and Arild Waller, editors, TABLEAUX 09: Automated Reasoning with Analytic Tableaux and Related Methods, number 5607 in LNAI, pages 152-166. Springer, 2009. [ bib | .pdf ] |
| [14] | Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In Edmund Clarke and Andrei Voronkov, editors, Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2009), volume 6355 of LNAI, Dakar, Senegal, April 2010. Springer. [ bib | .pdf ] |
| [15] | Kaustuv Chaudhuri. Classical and intuitionistic subexponential logics are equally expressive. In Anuj Dawar and Helmut Veith, editors, CSL 2010: Computer Science Logic, volume 6247 of LNCS, pages 185-199, Brno, Czech Republic, August 2010. Springer. [ bib | DOI | http ] |
| [16] | Kaustuv Chaudhuri. Magically constraining the inverse method using dynamic polarity assignment. In Christian Fermüller and Andrei Voronkov, editors, Proc. 17th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 6397 of LNCS, pages 202-216, Yogyakarta, Indonesia, October 2010. Springer. [ bib | DOI | http ] |
| [17] | Kaustuv Chaudhuri and Joëlle Despeyroux. A hybrid linear logic for constrained transition systems with applications to molecular biology. Research Report inria-00402942, INRIA-HAL, 2009. [ bib | http ] |
| [18] | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. Verifying safety properties with the TLA+ proof system. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of LNAI, pages 142-148, Edinburgh, UK, July 2010. Springer. [ bib | DOI | http ] |
| [19] | Kaustuv Chaudhuri, Damien Doligez, Stephan Merz, and Leslie Lamport. The TLA+ proof system: Building a heterogeneous verification platform. In Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, and Jim Woodcock, editors, Proceedings of the 7th International Colloquium on Theoretical Aspects of Computing (ICTAC), volume 6256 of LNCS, page 44, Natal, Rio Grande do Norte, Brazil, September 2010. Springer. [ bib | DOI | http ] |
| [20] | Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The Focused Calculus of Structures. In Computer Science Logic: 20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs), pages 159-173. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, September 2011. [ bib | DOI | .pdf ] |
| [21] | Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong, editors, Fifth International Conference on Theoretical Computer Science, volume 273 of IFIP, pages 383-396. Springer, September 2008. [ bib | .pdf ] |
| [22] | Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. J. of Automated Reasoning, 40(2-3):133-177, March 2008. [ bib | http | .pdf ] |
| [23] | Agata Ciabattoni, Lutz Straßburger, and Kazushige Terui. Expanding the realm of systematic proof theory. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, CSL'09, volume 5771 of Lecture Notes in Computer Science, pages 163-178. Springer, 2009. [ bib | http ] |
| [24] | Roberto Di Cosmo and Dale Miller. Linear logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, 2006. [ bib | http ] |
| [25] | Olivier Delande. Symmetric Dialogue Games in the Proof Theory of Linear Logic. PhD thesis, Ecole Polytechnique, October 2009. [ bib | http ] |
| [26] | Olivier Delande and Dale Miller. A neutral approach to proof and refutation in MALL. In F. Pfenning, editor, 23th Symp. on Logic in Computer Science, pages 498-508. IEEE Computer Society Press, 2008. [ bib | .pdf ] |
| [27] | Olivier Delande, Dale Miller, and Alexis Saurin. Proof and refutation in MALL as a game. Annals of Pure and Applied Logic, 161(5):654-672, February 2010. [ bib | http | .pdf ] |
| [28] | Roy Dyckhoff and Stephane Lengrand. Call-by-value λ-calculus and LJQ. J. of Logic and Computation, 17(6):1109-1134, 2007. [ bib ] |
| [29] | M. J. Gabbay and J. Cheney. A sequent calculus for nominal logic. In 19uth Symp. on Logic in Computer Science, pages 139-148, 2004. [ bib | .pdf ] |
| [30] | Murdoch Gabbay and Stéphane Lengrand. The lambda-context calculus. In Brigitte Pientka and Carsten Schürmann, editors, Revisions from the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007), volume 196 of Electronic Notes in Theoretical Computer Science, pages 19-35, 2008. [ bib ] |
| [31] | Murdoch Gabbay and Stéphane Lengrand. The lambda-context calculus. Information and Computation, 207(12):1369-1400, 2009. [ bib ] |
| [32] | Murdoch J. Gabbay. Automating Fraenkel-Mostowski syntax. In TPHOLs, 15th International Conference on Theorem Proving in Higher Order Logics, August 2002. [ bib ] |
| [33] | Andrew Gacek. Relating nominal and higher-order abstract syntax specifications. In Proceedings of the 2010 Symposium on Principles and Practice of Declarative Programming, pages 177-186. ACM, July 2010. [ bib | .pdf ] |
| [34] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Combining generic judgments with recursive definitions. In F. Pfenning, editor, 23th Symp. on Logic in Computer Science, pages 33-44. IEEE Computer Society Press, 2008. [ bib | .pdf ] |
| [35] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Reasoning in Abella about structural operational semantics specifications. In A. Abel and C. Urban, editors, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), number 228 in ENTCS, pages 85-100, 2008. [ bib | http | .pdf ] |
| [36] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. Accepted to the J. of Automated Reasoning, August 2010. [ bib | http ] |
| [37] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. [ bib | http ] |
| [38] | Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. A non-local method for robustness analysis of floating point programs. Technical report, INRIA, Tallinn, Estonie, February 2012. To appear in QAPL 2012. [ bib | http | .pdf ] |
| [39] | Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: the exponentials and splitting. Mathematical Structures in Computer Science, 21(3):563-584, 2011. [ bib ] |
| [40] | Anders Starcke Henriksen. Using LJF as a Framework for Proof Systems. Technical Report, University of Copenhagen, 2009. [ bib | http ] |
| [41] | Stefan Hetzl. On the form of witness terms. Draft manuscript, 2009. [ bib ] |
| [42] | Kentaro Kikuchi and Stéphane Lengrand. Strong normalisation of cut-elimination that simulates β-reduction. In Roberto Amadio, editor, 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'08), volume 4962 of LNCS, pages 380-394, Budapest, Hungary, March 2008. Springer. [ bib | .pdf ] |
| [43] | François Lamarche and Lutz Straßburger. From proof nets to the free *-autonomous category. Logical Methods in Computer Science, 2(4:3):1-44, 2006. [ bib | http ] |
| [44] | Gary T. Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler, Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith, and Aaron Stump. Roadmap for enhanced languages and methods to aid verification. In Fifth International Conference on Generative Programming and Component Engineering (GPCE), pages 221-235. ACM, October 2006. [ bib ] |
| [45] | Stéphane Lengrand. Termination of lambda-calculus with the extra call-by-value rule known as assoc. Technical report, CNRS-Ecole Polytechnique-INRIA, 2007. CoRR, abs/0806.4859. [ bib | http ] |
| [46] | Stéphane Lengrand, Roy Dyckhoff, and James McKinna. A focused sequent calculus framework for proof search in pure type systems. Logical Methods in Computer Science, 2010. [ bib | .pdf ] |
| [47] | Stéphane Lengrand and Alexandre Miquel. Classical Fω, orthogonality and symmetric candidates. Annals of Pure and Applied Logic, 153:3-20, March 2008. [ bib ] |
| [48] | Chuck Liang and Dale Miller. Focusing and polarization in intuitionistic logic. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 451-465. Springer, 2007. [ bib | .pdf ] |
| [49] | Chuck Liang and Dale Miller. On focusing and polarities in linear logic and intuitionistic logic. Extended version of accepted paper., September 2007. [ bib | http | .pdf ] |
| [50] | Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. [ bib | http ] |
| [51] | Chuck Liang and Dale Miller. A unified sequent calculus for focused proofs. In 24th Symp. on Logic in Computer Science, pages 355-364, 2009. [ bib | .pdf ] |
| [52] | Chuck Liang and Dale Miller. A focused approach to combining logics. Annals of Pure and Applied Logic, 162(9):679-697, 2011. [ bib | DOI | http | .pdf ] |
| [53] | Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. on Computational Logic, 3(1):80-136, 2002. [ bib | .pdf ] |
| [54] | Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. Theoretical Computer Science, 294(3):411-437, 2003. [ bib | .dvi | .ps | .pdf ] |
| [55] | Dale Miller. Higher-order quantification and proof search. In Hélène Kirchner and Christophe Ringeissen, editors, Proceedings of AMAST 2002, number 2422 in LNCS, pages 60-74, 2002. [ bib | .pdf ] |
| [56] | Dale Miller. Higher-order quantification and proof search: an extended abstract, July 2002. Presented at Linear Logic 2002, FLoC, Copenhagen. [ bib ] |
| [57] | Dale Miller. Definitions, unification, and the sequent calculus. In J. Levy, M. Kohlhase, J. Niehren, and M. Villaret, editors, Proceedings of the 17th International Workshop on Unification, UNIF'03, Technical Report DSIC-II/12/03, pages 1-2. Departamento de Sistemas Informàtics i Computació Universidad Politècnica de València, June 2003. Invited talk. [ bib ] |
| [58] | Dale Miller. Encryption as an abstract data type. In Ruy de Queiroz, Elaine Pimentel, and Lucilia Figueiredo, editors, WoLLIC'2003, 10th Workshop on Logic, Language, Information and Computation, volume 84 of ENTCS. Elsevier, 2003. Invited talk. [ bib ] |
| [59] | Dale Miller. Encryption as an abstract data-type: An extended abstract. In Iliano Cervesato, editor, Proceedings of FCS'03: Foundations of Computer Security, pages 3-14, 2003. [ bib | .dvi | .ps | .pdf ] |
| [60] | Dale Miller. Reasoning about proof search specifications: An abstract. In Theorem Proving in Higher Order Logics: 16th International Conference, TPHOLs 2003, volume 2758 of LNCS, page 204. Springer, 2003. Invited speaker. [ bib | .dvi | .pdf ] |
| [61] | Dale Miller. Bindings, mobility of bindings, and the -quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, 18th International Conference on Computer Science Logic (CSL) 2004, volume 3210 of LNCS, page 24, 2004. [ bib | .pdf ] |
| [62] | Dale Miller. Overview of linear logic programming. In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Phil Scott, editors, Linear Logic in Computer Science, volume 316 of London Mathematical Society Lecture Note, pages 119-150. Cambridge University Press, 2004. [ bib | .dvi | .ps | .pdf ] |
| [63] | Dale Miller. Collection analysis for Horn clause programs. In Proceedings of PPDP 2006: 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 179-188, July 2006. [ bib | .ps | .pdf ] |
| [64] | Dale Miller. Logic and logic programming: A personal account. ALP Newsletter, February 2006. Vol. 19, No. 1. [ bib | .pdf ] |
| [65] | Dale Miller. Representing and reasoning with operational semantics. In U. Furbach and N. Shankar, editors, Proceedings of IJCAR: International Joint Conference on Automated Reasoning, volume 4130 of LNAI, pages 4-20, August 2006. [ bib | .dvi | .pdf ] |
| [66] | Dale Miller. Formalizing operational semantic specifications in logic. Concurrency Column of the Bulletin of the EATCS, October 2008. [ bib | .pdf ] |
| [67] | Dale Miller. A proof-theoretic approach to the static analysis of logic programs. In Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, number 17 in Studies in Logic, pages 423-442. College Publications, 2008. [ bib | .pdf ] |
| [68] | Dale Miller. Formalizing operational semantic specifications in logic. In Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), volume 246, pages 147-165, August 2009. [ bib | http ] |
| [69] | Dale Miller. Finding unity in computational logic. In ACM-BCS-Visions Conference, April 2010. [ bib | .pdf ] |
| [70] | Dale Miller. Reasoning about computations using two-levels of logic. In K. Ueda, editor, Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS'10), number 6461 in LNCS, pages 34-46, 2010. [ bib | .pdf ] |
| [71] | Dale Miller. A proposal for broad spectrum proof certificates. In J.-P. Jouannaud and Z. Shao, editors, CPP: First International Conference on Certified Programs and Proofs, volume 7086 of LNCS, pages 54-69, 2011. [ bib | .pdf ] |
| [72] | Dale Miller and Vivek Nigam. Incorporating tables into proofs. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 466-480. Springer, 2007. [ bib | .pdf ] |
| [73] | Dale Miller and Elaine Pimentel. Using linear logic to reason about sequent systems. In Uwe Egly and Christian G. Fermüller, editors, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 2381 of LNCS, pages 2-23. Springer, 2002. [ bib | .dvi | .pdf ] |
| [74] | Dale Miller and Elaine Pimentel. Linear logic as a framework for specifying sequent calculus. In Jan van Eijck, Vincent van Oostrom, and Albert Visser, editors, Logic Colloquium '99: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Lecture Notes in Logic, pages 111-135. A K Peters Ltd, 2004. [ bib | .dvi | .ps | .pdf ] |
| [75] | Dale Miller and Alexis Saurin. A game semantics for proof search: Preliminary results. In Dan Ghica and Guy McCusker, editors, GaLoP 2005: Games for Logic and Programming Languages, 2005. [ bib ] |
| [76] | Dale Miller and Alexis Saurin. A game semantics for proof search: Preliminary results. In Proceedings of the Mathematical Foundations of Programming Semantics (MFPS05), number 155 in ENTCS, pages 543-563, 2006. [ bib | .pdf ] |
| [77] | Dale Miller and Alexis Saurin. From proofs to focused proofs: a modular proof of focalization in linear logic. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 405-419. Springer, 2007. [ bib | .pdf ] |
| [78] | Dale Miller and Alwen Tiu. Encoding generic judgments. In Proceedings of FSTTCS, number 2556 in LNCS, pages 18-32. Springer, December 2002. [ bib | .dvi | .pdf ] |
| [79] | Dale Miller and Alwen Tiu. A proof theory for generic judgments: An extended abstract. In Phokion Kolaitis, editor, 18th Symp. on Logic in Computer Science, pages 118-127. IEEE, June 2003. [ bib | .dvi | .ps | .pdf ] |
| [80] | Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749-783, October 2005. [ bib | .pdf ] |
| [81] | Alberto Momigliano and Alwen Tiu. Induction and co-induction in sequent calculus. In Mario Coppo, Stefano Berardi, and Ferruccio Damiani, editors, Post-proceedings of TYPES 2003, number 3085 in LNCS, pages 293-308, January 2003. [ bib | .pdf ] |
| [82] | Vivek Nigam. Using tables to construct non-redundant proofs. In CiE 2008: Abstracts and extended abstracts of unpublished papers, 2008. [ bib | .pdf ] |
| [83] | Vivek Nigam. Exploiting non-canonicity in the sequent calculus. PhD thesis, Ecole Polytechnique, September 2009. [ bib | .pdf ] |
| [84] | Vivek Nigam and Dale Miller. Focusing in linear meta-logic. In Proceedings of IJCAR: International Joint Conference on Automated Reasoning, volume 5195 of LNAI, pages 507-522. Springer, 2008. [ bib | http ] |
| [85] | Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pages 129-140, 2009. [ bib | .pdf ] |
| [86] | Vivek Nigam and Dale Miller. A framework for proof systems. J. of Automated Reasoning, 45(2):157-188, 2010. [ bib | http | .pdf ] |
| [87] | Michele Pagani and Alexis Saurin. Stream associative nets and lambda-mu-calculus. Technical Report 6431, INRIA, January 2008. [ bib | http ] |
| [88] | Elaine Pimentel and Dale Miller. On the specification of sequent systems. In LPAR 2005: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, number 3835 in LNAI, pages 352-366, 2005. [ bib | .pdf ] |
| [89] | Alexis Saurin. Separation with streams in the λμ-calculus. In 20th Symp. on Logic in Computer Science, pages 356-365. IEEE Computer Society, 2005. [ bib ] |
| [90] | Alexis Saurin. Typing streams in the Λμ-calculus: extended abstract. In Proceedings of the Short Papers Session at LPAR 2007, October 2007. [ bib | .pdf ] |
| [91] | Alexis Saurin. On the relations between the syntactic theories of λμ-calculi. In 17th EACSL Annual Conference on Computer Science Logic 2008 (CSL 2008), LNCS. Spring, September 2008. To appear. [ bib | .pdf ] |
| [92] | Alexis Saurin. Towards ludics programming: Interactive proof search. In Logic Programming, 24th International Conference, volume 5366 of LNCS, pages 253-268, December 2008. [ bib | .pdf ] |
| [93] | Alexis Saurin. Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique). PhD thesis, Ecole Polytechnique, September 2008. [ bib | http ] |
| [94] | Alexis Saurin. Typing streams in Λμ-calculus. ACM Transactions on Computational Logic, 11(4), 2010. [ bib | .pdf ] |
| [95] | M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. FreshML: Programming with binders made simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pages 263-274. ACM Press, August 2003. [ bib ] |
| [96] | Lutz Straßburger. Proof nets and the identity of proofs. Research Report 6013, INRIA, October 2006. Lecture notes for ESSLLI'06. [ bib | http ] |
| [97] | Lutz Straßburger. What could a boolean category be? In Steffen van Bakel, editor, Classical Logic and Computation 2006 (Satellite Workshop of ICALP'06), 2006. [ bib | .pdf ] |
| [98] | Lutz Straßburger. A characterisation of medial as rewriting rule. In Franz Baader, editor, Term Rewriting and Applications, RTA'07, volume 4533 of LNCS, pages 344-358. Springer, 2007. [ bib | .pdf ] |
| [99] | Lutz Straßburger. Deep inference for hybrid logic. In International Workshop on Hybrid Logic 2007 (Part of ESSLLI'07), 2007. [ bib | .pdf ] |
| [100] | Lutz Straßburger. On the axiomatisation of Boolean categories with and without medial. Theory and Applications of Categories, 18(18):536-601, 2007. [ bib | http | .pdf ] |
| [101] | Lutz Straßburger. Extension without cut. Draft manuscript, 2009. [ bib | .pdf ] |
| [102] | Lutz Straßburger. A kleene theorem for forest languages. In Adrian Horia Dediu, Armand-Mihai Ionescu, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications, LATA'09, volume 5457 of LNCS, pages 715-727. Springer, 2009. [ bib | http ] |
| [103] | Lutz Straßburger. Some observations on the proof theory of second order propositional multiplicative linear logic. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, TLCA'09, volume 5608 of LNCS, pages 309-324. Springer, 2009. [ bib | http ] |
| [104] | Lutz Straßburger. What is the problem with proof nets for classical logic? In Fernando Ferreira, Benedikt Löwe, Elvira Mayordomo, and Luís Mendes Gomes, editors, Programs, Proofs, Processes, 6th Conference on Computability in Europe (CiE 2010), volume 6158 of LNCS, pages 406-416, Ponta Delgada, Azores, Portugal, June 2010. Springer. [ bib | DOI | .pdf ] |
| [105] | Lutz Straßburger. From deep inference to proof nets via cut elimination. J. of Logic and Computation, 21(4):589-624, August 2011. [ bib ] |
| [106] | Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: The exponentials and decomposition. ACM Trans. Comput. Log., 12(4):23, 2011. [ bib ] |
| [107] | Alwen Tiu. Cut-elimination for a logic with generic judgments. Draft, available via web., January 2003. [ bib | .pdf ] |
| [108] | Alwen Tiu. Level 0/1 Prover: A tutorial, September 2004. Available online. [ bib ] |
| [109] | Alwen Tiu. A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University, May 2004. [ bib | http | .pdf ] |
| [110] | Alwen Tiu and Dale Miller. A proof search specification of the π-calculus. In 3rd Workshop on the Foundations of Global Ubiquitous Computing, volume 138 of ENTCS, pages 79-101, September 2004. [ bib | .pdf ] |
| [111] | Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. on Computational Logic, 11(2), 2010. [ bib | http ] |
| [112] | Alwen Tiu, Gopalan Nadathur, and Dale Miller. Mixing finite success and finite failure in an automated prover. In Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05), pages 79-98, December 2005. [ bib | .pdf ] |
| [113] | Alwen F. Tiu. An extension of L-lambda unification. Draft, available via web., September 2002. [ bib | .dvi | .pdf ] |
| [114] | C. Urban, A. M. Pitts, and M. J. Gabbay. Nominal unification. In M. Baaz, editor, Computer Science Logic and 8th Kurt Gödel Colloquium (CSL'03 & KGC), Vienna, Austria. Proccedings, LNCS, pages 513-527. Springer, Berlin, 2003. [ bib ] |
| [115] | Axelle Ziegler. Un format pour que la bisimulation soit une congruence dans les langages de processus avec mobilité. Technical report, INRIA Futurs, LIX and ENS, 2004. [ bib | .pdf ] |
| [116] | Axelle Ziegler, Dale Miller, and Catuscia Palamidessi. A congruence format for name-passing calculi. In Structural Operational Semantics (SOS'05), ENTCS, pages 169-189, Lisbon, Portugal, July 2005. Elsevier Science B.V. [ bib | .pdf ] |
This file was generated by bibtex2html 1.94.