Bibliography by Date

[1] Dale Miller. A system of inference based on proof search: an extended abstract. In Igor Walukiewicz, editor, Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), pages 1--11, 2023. [ bib | DOI ]
[2] Dale Miller and Jui-Hsuan Wu. A positive perspective on term representations. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1--3:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI ]
[3] Dale Miller. Proof theory, proof search, and logic programming. Unpublished monograph, December 2022. [ bib | .pdf ]
[4] Dale Miller. A survey of the proof-theoretic foundations of logic programming. Theory and Practice of Logic Programming, 22(6):859--904, October 2022. Published online November 2021. [ bib | DOI ]
[5] Dale Miller and Jui-Hsuan Wu. A positive perspective on term representations: Extended paper. Technical report, Inria, 2022. [ bib | http ]
[6] Dale Miller and Alexandre Viel. Proof search when equality is a logical connective. Annals of Mathematics and Artificial Intelligence, 90(5):523--535, 2022. Appears in the Special Issue on Theoretical and Practical Aspects of Unification. [ bib | DOI ]
[7] Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. From axioms to synthetic inference rules via focusing. Annals of Pure and Applied Logic, 173(5):1--32, 2022. [ bib | DOI ]
[8] Matteo Manighetti and Dale Miller. Computational logic based on linear logic and fixed points. Technical Report hal-03579451, HAL, 2022. [ bib | http ]
[9] Tomer Libal and Dale Miller. Functions-as-constructors higher-order unification: extended pattern unification. Annals of Mathematics and Artificial Intelligence, 90(5):455--479, 2022. Appears in the Special Issue on Theoretical and Practical Aspects of Unification. [ bib | DOI ]
[10] Chuck Liang and Dale Miller. Focusing Gentzen's LK proof system. In Thomas Piecha and Kai Wehmeier, editors, Peter Schroeder-Heister on Proof-Theoretic Semantics, Outstanding Contributions to Logic. Springer, 2022. To appear. [ bib | http ]
[11] Dale Miller. Reciprocal influences between logic programming and proof theory. Philosophy & Technology, 34(1):75--104, March 2021. [ bib | DOI ]
[12] Matteo Manighetti, Dale Miller, and Alberto Momigliano. Two Applications of Logic Programming to Coq. In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, 26th International Conference on Types for Proofs and Programs (TYPES 2020), volume 188 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1--10:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. [ bib | DOI | http ]
[13] Matteo Cimini, Dale Miller, and Jeremy G. Siek. Extrinsically typed operational semantics for functional languages. In Laurence Tratt and Juan de Lara, editors, ACM SIGPLAN International Conference on Software Language Engineering (SLE), pages 108--125. ACM SIGPLAN, ACM, November 2020. [ bib | DOI ]
[14] Roberto Blanco, Matteo Manighetti, and Dale Miller. FPC-coq: Using ELPI to elaborate external proof evidence into coq proofs. Technical Report hal-02974002, Inria, July 2020. Presented at the Coq Workshop 2020. [ bib | http ]
[15] Dale Miller. Andre and the early days of penn’s logic and computation group. In Vivek Nigam et al., editor, Logic, Language, and Security, number 12300 in lncs. pub-sv, 2020. [ bib | DOI ]
[16] Dale Miller. A distributed and trusted web of formal proofs. In D. V. Hung and M. D'Souza, editors, Distributed Computing and Internet Technology (ICDCIT), number 11969 in LNCS, pages 21--40. Springer, 2020. [ bib | DOI | http ]
[17] Dale Miller. My colleague, wife, and friend. In Mário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, and Frank Valencia, editors, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, number 11769 in lncs, pages xv--xvii. pub-sv, November 2019. [ bib | DOI ]
[18] Dale Miller. Mechanized metatheory revisited. Journal of Automated Reasoning, 63(3):625--665, October 2019. [ bib | DOI ]
[19] Ulysse Gérard, Dale Miller, and Gabriel Scherer. Functional programming with λ-tree syntax. In E. Komendantskaya, editor, Principles and Practice of Programming Languages 2019 (PPDP '19), October 2019. [ bib | DOI | http ]
[20] Roberto Blanco, Dale Miller, and Alberto Momigliano. Property-based testing via proof reconstruction. In E. Komendantskaya, editor, Principles and Practice of Programming Languages 2019 (PPDP '19), October 2019. [ bib | DOI ]
[21] Quentin Heath and Dale Miller. A proof theory for model checking. J. of Automated Reasoning, 63(4):857--885, 2019. [ bib | DOI ]
[22] Roberto Di Cosmo and Dale Miller. Linear logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2019 edition, 2019. [ bib ]
[23] 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 ]
[24] Ulysse Gérard and Dale Miller. Functional programming with λ-tree syntax: Draft. Available from https://trymlts.github.io/., May 2018. [ bib ]
[25] Ulysse Gérard, Dale Miller, and Gabriel Scherer. Try MLTS online, March 2018. https://trymlts.github.io/. [ bib ]
[26] Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić, editors, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), volume 97 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1--1:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | http ]
[27] Dale Miller. Proof checking and logic programming. Formal Aspects of Computing, 29(3):383--399, 2017. [ bib | DOI | http | .pdf ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] 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 ]
[32] 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 ]
[33] Zakaria Chihani, Dale Miller, and Fabien Renaud. A semantic framework for proof evidence. J. of Automated Reasoning, 59(3):287--330, 2017. [ bib | DOI ]
[34] 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 ]
[35] 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 LNCS, pages 255--273. Springer, 2017. [ bib | DOI ]
[36] 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 ]
[37] Zakaria Chihani, Danko Ilik, and Dale Miller. Classical polarizations yield double-negation translations. Technical report, Inria Saclay, August 2016. [ bib | http | .pdf ]
[38] 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 ]
[39] 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), pages 26:1--26:17, 2016. [ bib | DOI | .pdf ]
[40] Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics. Theoretical Computer Science, 655:92--108, 2016. [ bib | DOI ]
[41] 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, pages 93--108. Elsevier, 2016. [ bib | DOI ]
[42] 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 ]
[43] 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 ]
[44] 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 ]
[45] 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 ]
[46] 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 ]
[47] 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 ]
[48] 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 ]
[49] 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 ]
[50] 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 ]
[51] 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 ]
[52] 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 ]
[53] 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 ]
[54] 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):1--89, 2014. [ bib | DOI ]
[55] 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 | http ]
[56] 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 | DOI | .pdf ]
[57] 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 ]
[58] Dale Miller and Alwen Tiu. Extracting proofs from tabled proof search: Extended version. Technical report, INRIA-HAL, 2013. [ bib | http ]
[59] Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, 474:98--116, 2013. [ bib | DOI | http ]
[60] 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 | DOI | http ]
[61] 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 ]
[62] 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 ]
[63] 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 ]
[64] 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 ]
[65] 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 ]
[66] Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, June 2012. [ bib | DOI ]
[67] 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 ]
[68] 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 ]
[69] 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 ]
[70] Dale Miller. ProofCert: Broad spectrum proof certificates. An ERC Advanced Grant funded for the five years 2012-2016, February 2011. [ 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 | DOI | .pdf ]
[72] 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 ]
[73] Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48--73, 2011. [ bib | DOI | http ]
[74] Alexandre Viel and Dale Miller. Proof search when equality is a logical connective. Unpublished draft presented to the International Workshop on Proof-Search in Type Theories, July 2010. [ bib | .pdf ]
[75] 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 ]
[76] 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 ]
[77] Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. on Computational Logic, 11(2):13:1--13:35, 2010. [ bib | DOI ]
[78] Vivek Nigam and Dale Miller. A framework for proof systems. J. of Automated Reasoning, 45(2):157--188, 2010. [ bib | http | .pdf ]
[79] 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 ]
[80] 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 ]
[81] 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 ]
[82] Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Technical report, CoRR, August 2009. Extended version LICS 2008 paper. Submitted. [ bib | http ]
[83] 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 ]
[84] Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In António Porto and Francisco Javier López-Fraguas, editors, ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pages 129--140. ACM, 2009. [ bib | DOI ]
[85] Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747--4768, 2009. Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi. [ bib | DOI ]
[86] 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 ]
[87] Dale Miller. Formalizing operational semantic specifications in logic. Concurrency Column of the Bulletin of the EATCS, October 2008. [ bib | .pdf ]
[88] 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 | DOI ]
[89] Vivek Nigam and Dale Miller. Focusing in linear meta-logic: Extended report. Technical report, 2008. [ bib | http ]
[90] Vivek Nigam and Dale Miller. Focusing in linear meta-logic. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Proceedings of IJCAR: International Joint Conference on Automated Reasoning, volume 5195 of LNAI, pages 507--522. Springer, 2008. [ bib | http ]
[91] Dale Miller and Vivek Nigam. Proofs with tables. Available via the authors web pages, 2008. [ bib ]
[92] Dale Miller. A proof-theoretic approach to the static analysis of logic programs. In Christoph Benzmüller, Chad E. Brown, Jörg Siekmann, and Richard Statman, editors, 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 ]
[93] 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 | DOI | .pdf ]
[94] 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 ]
[95] Olivier Delande and Dale Miller. A neutral approach to proof and refutation in MALL: extended report. Available via the authors web pages, 2008. [ bib ]
[96] 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 ]
[97] 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 ]
[98] 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 ]
[99] Zach Snow, David Baelde, and Dale Miller. Taci: an interactive theorem proving framework. OCaml code., 2007. [ bib | http ]
[100] 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 ]
[101] 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 ]
[102] 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 ]
[103] 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 ]
[104] 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 ]
[105] David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. A User Guide to Bedwyr, November 2006. [ bib | .pdf ]
[106] 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 | DOI ]
[107] 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. Springer, August 2006. [ bib | .pdf ]
[108] 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 | DOI | .pdf ]
[109] Dale Miller. Logic and logic programming: A personal account. ALP Newsletter, February 2006. Vol. 19, No. 1. [ bib | .pdf ]
[110] 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 ]
[111] Roberto Di Cosmo and Dale Miller. Linear logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, 2006. [ 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] Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749--783, October 2005. [ bib | DOI ]
[114] 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 ]
[115] 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 ]
[116] 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 ]
[117] 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 ]
[118] 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 ]
[119] 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 | .pdf ]
[120] 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 | .pdf ]
[121] 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 | DOI | .pdf ]
[122] 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 ]
[123] 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 | .pdf ]
[124] 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 ]
[125] 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 | .pdf ]
[126] Dale Miller. Encryption as an abstract data-type: An extended abstract. In Iliano Cervesato, editor, Proceedings of FCS'03: Foundations of Computer Security, volume 84 of ENTCS, pages 18--29. Elsevier, 2003. [ bib | DOI | .pdf ]
[127] Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. Theoretical Computer Science, 294(3):411--437, 2003. [ bib | DOI ]
[128] Dale Miller and Alwen Tiu. Encoding generic judgments. In Proceedings of FSTTCS, number 2556 in LNCS, pages 18--32. Springer, December 2002. [ bib | .pdf ]
[129] Dale Miller. Higher-order quantification and proof search: an extended abstract, July 2002. Presented at Linear Logic 2002, FLoC, Copenhagen. [ bib ]
[130] 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 | .pdf ]
[131] 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 ]
[132] 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 | DOI | .pdf ]
[133] 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 ]
[134] 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 ]
[135] Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91--119, 2000. [ bib | DOI ]
[136] Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. ACM Computing Surveys, 31, September 1999. [ bib | DOI ]
[137] 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 ]
[138] 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 ]
[139] Dale Miller. λProlog: an introduction to the language and its logic. Incomplete draft., 1998. [ bib | .pdf ]
[140] 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 ]
[141] 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 ]
[142] Dale Miller. Forum: A multiple-conclusion specification logic. Theoretical Computer Science, 165(1):201--232, 1996. [ bib | DOI ]
[143] Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus: Preliminary report. ENTCS, 3, 1996. [ bib ]
[144] 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 ]
[145] 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 ]
[146] 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. [ bib ]
[147] Gopalan Nadathur and Dale Miller. Higher-order logic programming. Technical Report CS-1994-38, Department of Computer Science, Duke University, 1994. [ bib ]
[148] 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 ]
[149] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327--365, 1994. [ bib | DOI ]
[150] 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 ]
[151] 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 ]
[152] 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 ]
[153] Dale Miller. A proposal for modules for λProlog: Preliminary draft. In Dale Miller, editor, Proceedings of the 1992 λProlog Workshop, 1992. [ bib ]
[154] Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321--358, 1992. [ bib | DOI | .pdf ]
[155] Dale Miller. Logic, higher-order. In S. Shapiro, editor, Second Edition of the Encyclopedia of Artificial Intelligence. Wiley, 1992. [ bib ]
[156] John Hannan and Dale Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415--459, 1992. [ bib | DOI ]
[157] Dale Miller. Proof theory as an alternative to model theory. Newsletter of the Association for Logic Programming, 4(3), August 1991. Guest editorial. [ bib | .html ]
[158] 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. IEEE. [ bib ]
[159] Dale Miller. Unification of simply typed lambda-terms as logic programming. In Koichi Furukawa, editor, Eighth International Logic Programming Conference, pages 255--269, Paris, France, June 1991. MIT Press. [ bib ]
[160] 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 | DOI ]
[161] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Lars-Henrik Eriksson, Lars Hallnäs, and Peter Schroeder-Heister, editors, Extensions of Logic Programming: Second International Workshop, ELP '91, Stockholm, Sweden, January 27-29, 1991. Proceedings, volume 475 of LNAI, pages 253--281. Springer, 1991. [ bib ]
[162] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51(1--2):125--157, 1991. [ bib | DOI ]
[163] Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777--814, October 1990. [ bib | DOI ]
[164] 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 ]
[165] 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 ]
[166] 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 ]
[167] Dale Miller. Semantics of a simple meta-logic. Unpublished draft, March 1990. [ bib ]
[168] Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329--359. Academic Press, 1990. [ bib | .pdf ]
[169] 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 | DOI ]
[170] 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 ]
[171] 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 ]
[172] Dale Miller. Lexical scoping as universal quantification. In G. Levi and M. Martelli, editors, Sixth International Logic Programming Conference, pages 268--283, Lisbon, Portugal, June 1989. MIT Press. [ bib | .pdf ]
[173] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1-2):79--108, January 1989. [ bib | DOI ]
[174] 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 ]
[175] 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 ]
[176] 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 ]
[177] 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 ]
[178] Gopalan Nadathur and Dale Miller. An Overview of λProlog. In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810--827, Seattle, August 1988. MIT Press. [ bib | .pdf ]
[179] John Hannan and Dale Miller. Uses of higher-order unification for implementing program transformers. In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth International Logic Programming Conference, pages 942--959, Seattle, Washington, August 1988. MIT Press. [ bib ]
[180] Dale Miller and Gopalan Nadathur. λProlog Version 2.7. Distribution in C-Prolog and Quintus sources, July 1988. [ bib | http ]
[181] 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 ]
[182] Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ewing Lusk and Ross Overbeck, editors, Ninth International Conference on Automated Deduction, number 310 in LNCS, pages 61--80, Argonne, IL, May 1988. Springer. [ bib | DOI ]
[183] 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 ]
[184] Dale Miller and Gopalan Nadathur. λProlog Version 2.6. Distribution in C-Prolog sources, August 1987. [ bib ]
[185] 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 ]
[186] 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 ]
[187] Dale Miller. A compact representation of proofs. Studia Logica, 46(4):347--370, 1987. [ bib | DOI ]
[188] Amy Felty and Dale Miller. Proof explanation and revision. Draft, 1987. [ bib ]
[189] 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 ]
[190] Dale Miller and Amy Felty. An integration of resolution and natural deduction theorem proving. In Tom Kehler, Stan Rosenschein, Robert Filman, and Peter F. Patel-Schneider, editors, National Conference on Artificial Intelligence (AAAI-86), pages 198--202, Philadelphia, PA, August 1986. [ bib ]
[191] Dale Miller and Gopalan Nadathur. Higher-order logic programming. In Ehud Shapiro, editor, Proceedings of the Third International Logic Programming Conference, volume 225 of LNCS, pages 448--462, London, June 1986. Springer. [ bib | DOI ]
[192] 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 | DOI ]
[193] 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 ]
[194] 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 ]
[195] Peter B. Andrews, Eve Longini Cohen, Dale Miller, and Frank Pfenning. Automating higher order logic. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 169--192. American Mathematical Society, Providence, RI, 1984. [ bib ]
[196] Peter B. Andrews, Eve Longini-Cohen, Dale Miller, and Frank Pfenning. Automating higher order logics. Contemp. Math, 29:169--192, 1984. [ bib ]
[197] Dale Miller. Proofs in Higher-order Logic. PhD thesis, Carnegie-Mellon University, August 1983. [ bib | .pdf ]
[198] 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 ]

This file was generated by bibtex2html 1.99.