[ACMP84] | Peter B. Andrews, Eve Longini Cohen, Dale Miller, and Frank Pfenning. Automating higher order logic. In Automated Theorem Proving: After 25 Years, pages 169--192. American Mathematical Society, Providence, RI, 1984. [ bib ] |
[ALCMP84] | Peter B. Andrews, Eve Longini-Cohen, Dale Miller, and Frank Pfenning. Automating higher order logics. Contemp. Math, 29:169--192, 1984. [ bib ] |
[BCG^{+}14] | David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2), 2014. [ bib | DOI | http ] |
[BCM17] | Roberto Blanco, Zakaria Chihani, and Dale Miller. Translating between implicit and explicit versions of proof. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 255--273. Springer, 2017. [ bib | DOI ] |
[BGM^{+}06] | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. A User Guide to Bedwyr, November 2006. [ bib | .pdf ] |
[BGM^{+}07] | 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 | DOI | .pdf ] |
[BLM16] | Roberto Blanco, Tomer Libal, and Dale Miller. Defining the meaning of TPTP formatted proofs. In Boris Konev, Stephan Schulz, and Laurent Simon, editors, IWIL-2015. 11th International Workshop on the Implementation of Logics, volume 40 of EPiC Series in Computing, pages 78--90. EasyChair, 2016. [ bib | .html ] |
[BM07a] | 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 | DOI | .pdf ] |
[BM07b] | 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 ] |
[BM14] | Christoph Benzmüller and Dale Miller. Automation of higher-order logic. In J. Siekmann, editor, Computational Logic, volume 9 of Handbook of the History of Logic, pages 215--254. North Holland, 2014. [ bib | DOI ] |
[BM15] | Roberto Blanco and Dale Miller. Proof outlines as proof certificates: a system description. In Iliano Cervesato and Carsten Schürmann, editors, Proceedings First International Workshop on Focusing, volume 197 of Electronic Proceedings in Theoretical Computer Science, pages 7--14. Open Publishing Association, November 2015. [ bib | DOI | .html ] |
[BMM17] | Roberto Blanco, Dale Miller, and Alberto Momigliano. Property-based testing via proof reconstruction. In Marino Miculan and Florian Rabe, editors, Work-in-Progress Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Technical reports of DIMI, University of Udine, pages 17--22, 2017. [ bib | http ] |
[BMS10] | 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 | DOI | .pdf ] |
[BMSV09] | David Baelde, Dale Miller, Zach Snow, and Alexandre Viel. Tac: A generic and adaptable interactive theorem prover. http://slimmer.gforge.inria.fr/tac/, 2009. [ bib ] |
[CCM15] | Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pages 157--166, Mumbai, India, January 2015. ACM. [ bib | DOI | http ] |
[CHM12] | Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A systematic approach to canonicity in the classical sequent calculus. In Patrick Cégielski and Arnaud Durand, editors, CSL 2012: Computer Science Logic, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 183--197. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, September 2012. [ bib | DOI ] |
[CHM16] | Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A multi-focused proof system isomorphic to expansion proofs. J. of Logic and Computation, 26(2):577--603, 2016. [ bib | DOI | http | .pdf ] |
[CIM16] | Zakaria Chihani, Danko Ilik, and Dale Miller. Classical polarizations yield double-negation translations. Technical report, Inria Saclay, August 2016. [ bib | http | .pdf ] |
[CM06] | Roberto Di Cosmo and Dale Miller. Linear logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, 2006. [ bib | http ] |
[CM16] | Zakaria Chihani and Dale Miller. Proof certificates for equality reasoning. In Mario Benevides and René Thiemann, editors, Post-proceedings of LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications. Natal, Brazil., number 323 in ENTCS, 2016. [ bib | DOI ] |
[CMR13a] | Zakaria Chihani, Dale Miller, and Fabien Renaud. Checking foundational proof certificates for first-order logic (extended abstract). In J. C. Blanchette and J. Urban, editors, Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), volume 14 of EPiC Series, pages 58--66. EasyChair, 2013. [ bib ] |
[CMR13b] | Zakaria Chihani, Dale Miller, and Fabien Renaud. Foundational proof certificates in first-order logic. In Maria Paola Bonacina, editor, CADE 24: Conference on Automated Deduction 2013, number 7898 in LNAI, pages 162--177, 2013. [ bib | DOI ] |
[CMR16] | Zakaria Chihani, Dale Miller, and Fabien Renaud. Supporting λProlog code, April 2016. http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fpc-support.tar. [ bib ] |
[CMR17] | Zakaria Chihani, Dale Miller, and Fabien Renaud. A semantic framework for proof evidence. J. of Automated Reasoning, 59:287--330, 2017. [ bib | DOI ] |
[CMS08] | 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 ] |
[DM08a] | 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 | DOI | .pdf ] |
[DM08b] | Olivier Delande and Dale Miller. A neutral approach to proof and refutation in MALL: extended report. Available via the authors web pages, 2008. [ bib ] |
[DMS10] | 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 | DOI | .pdf ] |
[FM87] | Amy Felty and Dale Miller. Proof explanation and revision. Draft, 1987. [ bib ] |
[FM88] | Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, number 310 in LNCS, pages 61--80, Argonne, IL, May 1988. Springer. [ bib ] |
[FM89] | Amy Felty and Dale Miller. A meta language for type checking and inference: An extended abstract. Presented at the 1989 Workshop on Programming Logic, Bålstad, Sweden, 1989. [ bib ] |
[FM90] | Amy Felty and Dale Miller. Encoding a dependent-type λ-calculus in a logic programming language. In Mark Stickel, editor, Proceedings of the 1990 Conference on Automated Deduction, volume 449 of LNAI, pages 221--235. Springer, 1990. [ bib ] |
[GM17] | Ulysse Gérard and Dale Miller. Separating functional computation from relations. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pages 23:1--23:17, 2017. [ bib | DOI ] |
[GM18a] | Ulysse Gérard and Dale Miller. Functional programming with λ-tree syntax: a progress report. In 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Oxford, United Kingdom, July 2018. [ bib | http | .pdf ] |
[GM18b] | Ulysse Gérard and Dale Miller. TryMLTS. https://trymlts.github.io/, 2018. [ bib ] |
[GMN08a] | 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 ] |
[GMN08b] | 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 | DOI | .pdf ] |
[GMN09] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Technical report, CoRR, August 2009. Extended version LICS 2008 paper. Submitted. [ bib | http ] |
[GMN11] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48--73, 2011. [ bib | DOI | http ] |
[GMN12] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. J. of Automated Reasoning, 49(2):241--273, 2012. [ bib | DOI | http ] |
[GMP12a] | 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 ] |
[GMP12b] | Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. A non-local method for robustness analysis of floating point programs. In Herbert Wiklicky and Mieke Massink, editors, Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), volume 85 of Electronic Proceedings in Theoretical Computer Science, pages 63--76, 2012. [ bib | DOI ] |
[GMP12c] | Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Non-local robustness analysis via rewriting techniques. An earlier version of this paper appeared in the pre-proceedings of QFM 2012., September 2012. [ bib | .pdf ] |
[GMP13] | Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics. In Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), pages 1--18, 2013. [ bib | http ] |
[GMP16] | Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics. Theoretical Computer Science, 655:92--108, 2016. [ bib | DOI ] |
[HM88a] | John Hannan and Dale Miller. Enriching a meta-language with higher-order features. Technical Report MS-CIS-88-45, University of Pennsylvania, June 1988. [ bib | http ] |
[HM88b] | John Hannan and Dale Miller. Uses of higher-order unification for implementing program transformers. In Fifth International Logic Programming Conference, pages 942--959, Seattle, Washington, August 1988. MIT Press. [ bib ] |
[HM89a] | John Hannan and Dale Miller. Deriving mixed evaluation from standard evaluation for a simple functional programming language. In Jan L. A. van de Snepscheut, editor, 1989 Intern. Conf. on Mathematics of Program Construction, volume 375 of LNCS, pages 239--255. Springer, 1989. [ bib | .pdf ] |
[HM89b] | John Hannan and Dale Miller. A meta-logic for functional programming. In Harvey Abramson and M. H. Rogers, editors, Meta-Programming in Logic Programming, Computer Science and Intelligent Systems, chapter 24, pages 453--476. MIT Press, 1989. Proceedings of the 1988 Workshop on Meta-Programming in Logic Programming, Bristol, UK. [ bib ] |
[HM90a] | John Hannan and Dale Miller. From operational semantics to abstract machines: Preliminary results. In M. Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 323--332. ACM, ACM Press, 1990. [ bib ] |
[HM90b] | Joshua Hodas and Dale Miller. Representing objects in a logic programming language with scoping constructs. In David H. D. Warren and Peter Szeredi, editors, 1990 International Conference in Logic Programming, pages 511--526. MIT Press, June 1990. [ bib ] |
[HM91] | Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic: Extended abstract. In G. Kahn, editor, 6th Symp. on Logic in Computer Science, pages 32--42, Amsterdam, July 1991. [ bib ] |
[HM92] | John Hannan and Dale Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415--459, 1992. [ bib ] |
[HM94] | Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327--365, 1994. [ bib ] |
[HM15] | Quentin Heath and Dale Miller. A framework for proof certificates in finite state exploration. In Cezary Kaliszyk and Andrei Paskevich, editors, Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pages 11--26. Open Publishing Association, August 2015. [ bib | DOI | .pdf ] |
[HM17] | Quentin Heath and Dale Miller. A proof theory for model checking: An extended abstract. In Iliano Cervesato and Maribel Fernández, editors, Proceedings Fourth International Workshop on Linearity (LINEARITY 2016), volume 238 of EPTCS, January 2017. [ bib | DOI ] |
[HM18] | Quentin Heath and Dale Miller. A proof theory for model checking. J. of Automated Reasoning, 2018. To appear in a special issue for Linearity 2016. [ bib | DOI | .pdf ] |
[LAB^{+}06] | 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 ] |
[LM07a] | 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 ] |
[LM07b] | 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 ] |
[LM09a] | Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747--4768, 2009. [ bib | DOI ] |
[LM09b] | 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 ] |
[LM11] | Chuck Liang and Dale Miller. A focused approach to combining logics. Annals of Pure and Applied Logic, 162(9):679--697, 2011. [ bib | DOI | .pdf ] |
[LM13a] | Chuck Liang and Dale Miller. Kripke semantics and proof systems for combining intuitionistic logic and classical logic. Annals of Pure and Applied Logic, 164(2):86--111, February 2013. [ bib | DOI | http ] |
[LM13b] | Chuck Liang and Dale Miller. Unifying classical and intuitionistic logics for computational control. In Orna Kupferman, editor, 28th Symp. on Logic in Computer Science, pages 283--292, 2013. [ bib | .pdf ] |
[LM15] | Chuck Liang and Dale Miller. On subexponentials, synthetic connectives, and multi-level delimited control. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), number 9450 in LNCS, November 2015. [ bib | DOI | .pdf ] |
[LM16] | Tomer Libal and Dale Miller. Functions-as-constructors higher-order unification. In D. Kesner and B. Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), page 26:1–26:17, 2016. [ bib | DOI | .pdf ] |
[MCA82] | Dale A. Miller, Eve Longini Cohen, and Peter B. Andrews. A look at TPS. In Donald W. Loveland, editor, Sixth Conference on Automated Deduction, volume 138 of LNCS, pages 50--69, New York, 1982. Springer. [ bib ] |
[MF86] | Dale Miller and Amy Felty. An integration of resolution and natural deduction theorem proving. In National Conference on Artificial Intelligence (AAAI-86), pages 198--202, Philadelphia, PA, August 1986. [ bib ] |
[Mil83] | Dale Miller. Proofs in Higher-order Logic. PhD thesis, Carnegie-Mellon University, August 1983. [ bib | .pdf ] |
[Mil84] | Dale Miller. Expansion tree proofs and their conversion to natural deduction proofs. In R. E. Shostak, editor, Seventh Conference on Automated Deduction, volume 170 of LNCS, pages 375--393, Napa CA, May 1984. Springer. [ bib ] |
[Mil86] | Dale Miller. A theory of modules for logic programming. In Robert M. Keller, editor, Third Annual IEEE Symposium on Logic Programming, pages 106--114, Salt Lake City, Utah, September 1986. [ bib ] |
[Mil87a] | Dale Miller. A compact representation of proofs. Studia Logica, 46(4):347--370, 1987. [ bib ] |
[Mil87b] | Dale Miller. Hereditary Harrop formulas and logic programming. In Proceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science, pages 153--156, Moscow, August 1987. [ bib ] |
[Mil88] | Dale Miller. Logic programming based on higher-order hereditary Harrop formulas. Technical Report MS-CIS-88-77, Computer Science Department, University of Pennsylvania, September 1988. Transparencies for lectures at the Advanced School on Foundations of Logic Programming, Algehro, Sardinia. [ bib ] |
[Mil89a] | Dale Miller. Lexical scoping as universal quantification. In Sixth International Logic Programming Conference, pages 268--283, Lisbon, Portugal, June 1989. MIT Press. [ bib | .pdf ] |
[Mil89b] | Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification: Extended abstract. In Graham M. Birtwistle, editor, Proceedings of the 1989 Banff meeting on “Higher-Orders”, Banff, Canada, September 1989. [ bib ] |
[Mil89c] | Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1-2):79--108, January 1989. [ bib ] |
[Mil90a] | Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329--359. Academic Press, 1990. [ bib | .pdf ] |
[Mil90b] | Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Proceedings of the Logical Frameworks BRA Workshop, pages 323--335, Antibes, France, June 1990. Available as UPenn CIS technical report MS-CIS-90-59. [ bib | .pdf ] |
[Mil90c] | Dale Miller. Semantics of a simple meta-logic. Unpublished draft, March 1990. [ bib ] |
[Mil91a] | Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Peter Schroeder-Heister, editor, Extensions of Logic Programming: International Workshop, Tübingen, volume 475 of LNAI, pages 253--281. Springer, 1991. [ bib ] |
[Mil91b] | Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1(4):497--536, 1991. [ bib ] |
[Mil91c] | Dale Miller. Proof theory as an alternative to model theory. Newsletter of the Association for Logic Programming, August 1991. Guest editorial. [ bib | .html ] |
[Mil91d] | Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255--269, Paris, France, June 1991. MIT Press. [ bib ] |
[Mil92a] | Dale Miller. Abstract syntax and logic programming. In Logic Programming: Proceedings of the First Russian Conference on Logic Programming, 14-18 September 1990, number 592 in LNAI, pages 322--337. Springer, 1992. [ bib ] |
[Mil92b] | Dale Miller. Linear logic and logic programming: An overview. In Dale Miller, editor, Proceedings of the Workshop on Linear Logic and Logic Programming (Washington, DC), November 1992. Available as UPenn CIS technical report MS-CIS-92-80 and electronically from ftp.cis.upenn.edu in pub/meetings/LL+LP-proceedings. [ bib ] |
[Mil92c] | Dale Miller. Logic, higher-order. In S. Shapiro, editor, Second Edition of the Encyclopedia of Artificial Intelligence. Wiley, 1992. [ bib ] |
[Mil92d] | Dale Miller. A proposal for modules for λProlog: Preliminary draft. In Dale Miller, editor, Proceedings of the 1992 λProlog Workshop, 1992. [ bib ] |
[Mil92e] | Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321--358, 1992. [ bib | .pdf ] |
[Mil93] | Dale Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, 3rd Workshop on Extensions to Logic Programming, number 660 in LNCS, pages 242--265, Bologna, Italy, 1993. Springer. [ bib | .pdf ] |
[Mil94a] | Dale Miller. A multiple-conclusion meta-logic. In S. Abramsky, editor, 9th Symp. on Logic in Computer Science, pages 272--281, Paris, July 1994. IEEE Computer Society Press. [ bib ] |
[Mil94b] | Dale Miller. A proposal for modules in λProlog. In R. Dyckhoff, editor, 4th Workshop on Extensions to Logic Programming, number 798 in LNCS, pages 206--221. Springer, 1994. [ bib ] |
[Mil95a] | Dale Miller. Observations about using logic as a specification language. In M. Sessa, editor, Proceedings of GULP-PRODE'95: Joint Conference on Declarative Programming, Marina di Vietri (Salerno-Italy), September 1995. [ bib ] |
[Mil95b] | Dale Miller. A survey of linear logic programming. Computational Logic: The Newsletter of the European Network in Computational Logic, 2(2):63--67, December 1995. [ bib ] |
[Mil96] | Dale Miller. Forum: A multiple-conclusion specification logic. Theoretical Computer Science, 165(1):201--232, September 1996. [ bib ] |
[Mil97] | Dale Miller. Logic programming and meta-logic. In Helmut Schwichtenberg, editor, Logic of Computation, volume 157 of Nato ASI Series, pages 265--308. Springer, 1997. [ bib ] |
[Mil98] | Dale Miller. λProlog: an introduction to the language and its logic. Incomplete draft., 1998. [ bib | .pdf ] |
[Mil99] | Dale Miller. Sequent calculus and the specification of computation. In Ulrich Berger and Helmut Schwichtenberg, editors, Computational Logic, volume 165 of Nato ASI Series, pages 399--444. Springer, 1999. [ bib ] |
[Mil00] | Dale Miller. Abstract syntax for variable binders: An overview. In John Lloyd and et al., editors, CL 2000: Computational Logic, number 1861 in LNAI, pages 239--253. Springer, 2000. [ bib | .pdf ] |
[Mil01] | Dale Miller. Encoding generic judgments: Preliminary results. In R. L. Crole, S. J. Ambler, and A. Momigliano, editors, Proceedings of the MERLIN 2001 Workshop, Siena, volume 58 of ENTCS. Elsevier Science Publishers, 2001. [ bib ] |
[Mil02a] | 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 ] |
[Mil02b] | Dale Miller. Higher-order quantification and proof search: an extended abstract, July 2002. Presented at Linear Logic 2002, FLoC, Copenhagen. [ bib ] |
[Mil03a] | 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 ] |
[Mil03b] | 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 ] |
[Mil03c] | 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 ] |
[Mil03d] | 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 ] |
[Mil04a] | 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 ] |
[Mil04b] | 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 ] |
[Mil05] | Dale Miller. A proof theoretic approach to operational semantics. In Luca Aceto and Andrew D. Gordon, editors, Algebraic Process Calculi: The First Twenty Five Years and Beyond, pages 172--175. Bertinoro, Italy, August 2005. [ bib | .pdf ] |
[Mil06a] | 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 ] |
[Mil06b] | Dale Miller. Logic and logic programming: A personal account. ALP Newsletter, February 2006. Vol. 19, No. 1. [ bib | .pdf ] |
[Mil06c] | 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 ] |
[Mil08a] | Dale Miller. Formalizing operational semantic specifications in logic. Concurrency Column of the Bulletin of the EATCS, October 2008. [ bib | .pdf ] |
[Mil08b] | 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 ] |
[Mil09] | 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 | DOI ] |
[Mil10a] | Dale Miller. Finding unity in computational logic. In Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference, ACM-BCS '10, pages 3:1--3:13. British Computer Society, April 2010. [ bib | .pdf ] |
[Mil10b] | 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 ] |
[Mil11a] | Dale Miller. ProofCert: Broad spectrum proof certificates. An ERC Advanced Grant funded for the five years 2012-2016, February 2011. [ bib | .pdf ] |
[Mil11b] | 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 | DOI | .pdf ] |
[Mil13] | Dale Miller. Foundational proof certificates: Making proof universal and permanent. In Alberto Momigliano, Brigitte Pientka, and Randy Pollack, editors, Proceedings of the 2013 ACM SIGPLAN Workshop on Logical Frameworks & Meta-Languages: Theory & Practice, LFMTP'13, page 1. ACM, September 2013. [ bib | .pdf ] |
[Mil14] | Dale Miller. Communicating and trusting proofs: The case for broad spectrum proof certificates. In P. Schroeder-Heister, W. Hodges, G. Heinzmann, and P. E. Bour, editors, Logic, Methodology, and Philosophy of Science. Proceedings of the Fourteenth International Congress, pages 323--342. College Publications, 2014. [ bib ] |
[Mil15a] | Dale Miller. Foundational proof certificates. In David Delahaye and Bruno Woltzenlogel Paleo, editors, All about Proofs, Proofs for All, volume 55 of Mathematical Logic and Foundations, pages 150--163. College Publications, London, UK, January 2015. [ bib | .pdf ] |
[Mil15b] | Dale Miller. Proof checking and logic programming. In Moreno Falaschi, editor, Logic-Based Program Synthesis and Transformation (LOPSTR) 2015, number 9527 in LNCS, pages 3--17. Springer, 2015. [ bib | DOI ] |
[Mil15c] | Dale Miller. Proof checking and logic programming. In Elvira Albert, editor, ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), page 18. ACM, July 2015. [ bib | DOI ] |
[Mil17a] | Dale Miller. Expansion proofs. In Bruno Woltzenlogel Paleo, editor, Towards an Encyclopaedia of Proof Systems, page 18. College Publications, London, UK, 1 edition, January 2017. [ bib | .pdf ] |
[Mil17b] | Dale Miller. Focused LJ. In Bruno Woltzenlogel Paleo, editor, Towards an Encyclopaedia of Proof Systems, pages 68--69. College Publications, London, UK, 1 edition, January 2017. [ bib | .pdf ] |
[Mil17c] | Dale Miller. Focused LK. In Bruno Woltzenlogel Paleo, editor, Towards an Encyclopaedia of Proof Systems, pages 66--67. College Publications, London, UK, 1 edition, January 2017. [ bib | .pdf ] |
[Mil17d] | Dale Miller. Mechanized metatheory revisited: An extended abstract. In Post-proceedings of TYPES 2016, Novi Sad, Serbia, 2017. [ bib | http | .pdf ] |
[Mil17e] | Dale Miller. Proof checking and logic programming. Formal Aspects of Computing, 29(3):383--399, 2017. [ bib | DOI | http | .pdf ] |
[MM97] | Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In Glynn Winskel, editor, 12th Symp. on Logic in Computer Science, pages 434--445, Warsaw, Poland, July 1997. IEEE Computer Society Press. [ bib ] |
[MM00] | Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91--119, 2000. [ bib | DOI ] |
[MM02] | 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 ] |
[MMP96] | Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus: Preliminary report. ENTCS, 3, 1996. [ bib ] |
[MMP03] | 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 ] |
[MMV16] | Sonia Marin, Dale Miller, and Marco Volpe. A focused framework for emulating modal proof systems. In Lev Beklemishev, Stéphane Demri, and András Máté, editors, 11th Conference on Advances in Modal Logic, number 11 in Advances in Modal Logic, pages 469--488, Budapest, Hungary, August 2016. College Publications. [ bib | http | .pdf ] |
[MN85] | Dale Miller and Gopalan Nadathur. A computational logic approach to syntax and semantics. Presented at the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985. [ bib ] |
[MN86a] | Dale Miller and Gopalan Nadathur. Higher-order logic programming. In Ehud Shapiro, editor, Proceedings of the Third International Logic Programming Conference, pages 448--462, London, June 1986. [ bib | DOI ] |
[MN86b] | Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pages 247--255. Association for Computational Linguistics, Morristown, New Jersey, 1986. [ bib ] |
[MN87a] | Dale Miller and Gopalan Nadathur. λProlog Version 2.6. Distribution in C-Prolog sources, August 1987. [ bib ] |
[MN87b] | Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379--388, San Francisco, September 1987. [ bib | .pdf ] |
[MN88] | Dale Miller and Gopalan Nadathur. λProlog Version 2.7. Distribution in C-Prolog and Quintus sources, July 1988. [ bib | http ] |
[MN07] | 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 | DOI | .pdf ] |
[MN08] | Dale Miller and Vivek Nigam. Proofs with tables. Available via the authors web pages, 2008. [ bib ] |
[MN12] | Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, June 2012. [ bib | DOI ] |
[MNPS91] | Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125--157, 1991. [ bib ] |
[MNS87] | Dale Miller, Gopalan Nadathur, and Andre Scedrov. Hereditary Harrop formulas and uniform proof systems. In David Gries, editor, 2nd Symp. on Logic in Computer Science, pages 98--105, Ithaca, NY, June 1987. [ bib ] |
[MP99] | Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. ACM Computing Surveys, 31, September 1999. [ bib ] |
[MP02] | 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 ] |
[MP04] | 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 ] |
[MP13] | Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, 474:98--116, 2013. [ bib | DOI | http ] |
[MS05] | 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 ] |
[MS06] | 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 ] |
[MS07] | 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 ] |
[MT02] | 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 ] |
[MT03] | 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 ] |
[MT05] | Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749--783, October 2005. [ bib | DOI | .pdf ] |
[MT13a] | Dale Miller and Alwen Tiu. Extracting proofs from tabled proof search. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs, number 8307 in LNCS, pages 194--210, Melburne, Australia, December 2013. Springer. [ bib | .pdf ] |
[MT13b] | Dale Miller and Alwen Tiu. Extracting proofs from tabled proof search: Extended version. Technical report, INRIA-HAL, 2013. [ bib | http ] |
[MV15] | Dale Miller and Marco Volpe. Focused labeled proof systems for modal logic. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), number 9450 in LNCS, pages 266--280, November 2015. [ bib | DOI ] |
[NM88] | Gopalan Nadathur and Dale Miller. An Overview of λProlog. In Fifth International Logic Programming Conference, pages 810--827, Seattle, August 1988. MIT Press. [ bib | .pdf ] |
[NM90] | Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777--814, October 1990. [ bib ] |
[NM94] | Gopalan Nadathur and Dale Miller. Higher-order logic programming. Technical Report CS-1994-38, Department of Computer Science, Duke University, 1994. [ bib ] |
[NM98] | Gopalan Nadathur and Dale Miller. Higher-order logic programming. In Dov M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 499--590. Clarendon Press, Oxford, 1998. [ bib ] |
[NM08a] | 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 ] |
[NM08b] | Vivek Nigam and Dale Miller. Focusing in linear meta-logic: Extended report. Technical report, 2008. [ bib | http ] |
[NM09] | 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 ] |
[NM10] | Vivek Nigam and Dale Miller. A framework for proof systems. J. of Automated Reasoning, 45(2):157--188, 2010. [ bib | http | .pdf ] |
[PM90] | Remo Pareschi and Dale Miller. Extending definite clause grammars with scoping constructs. In David H. D. Warren and Peter Szeredi, editors, 1990 International Conference in Logic Programming, pages 373--389. MIT Press, June 1990. [ bib ] |
[PM05] | 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 ] |
[SBM07] | Zach Snow, David Baelde, and Dale Miller. Taci: an interactive theorem proving framework. OCaml code., 2007. [ bib | http ] |
[TM05] | 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, 2005. [ bib | DOI | .pdf ] |
[TM10] | 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 | DOI | http ] |
[TNM05] | 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 ] |
[VM10] | Alexandre Viel and Dale Miller. Proof search when equality is a logical connective. Presented to the International Workshop on Proof-Search in Type Theories, July 2010. [ bib | .pdf ] |
[ZMP05] | 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.98.