Dale Miller - RankMe

174 papers A* 13A 13B 34C 7Misc 2Journal 55Unranked 42

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Book Announcement: Proof Theory and Logic Programming: Computation as Proof Search. ACM SIGLOG News Dale Miller
2025	B	`conf`	Designing a Safe Forward Chaining Tactic Using Productive Proofs. TABLEAUX Kaustuv Chaudhuri, Arunava Gantait, Dale Miller
2025	B	`conf`	Linear Logic Using Negative Connectives. FSCD Dale Miller
2025	J	`jnl`	Peano Arithmetic and μMALL. Fundam. Informaticae Matteo Manighetti, Dale Miller
2024	—	`ch.`	About Trust and Proof: An Experimental Framework for Heterogeneous Verification. The Practice of Formal Methods (II) Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller
2024	Misc	`ed.`	Functional and Logic Programming - 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024, Proceedings FLOPS Jeremy Gibbons, Dale Miller
2024	J	`jnl`	Property-Based Testing by Elaborating Proof Outlines. CoRR Dale Miller, Alberto Momigliano
2024	J	`jnl`	Property-Based Testing by Elaborating Proof Outlines. Theory Pract. Log. Program. Dale Miller, Alberto Momigliano
2023	B	`conf`	A Positive Perspective on Term Representation (Invited Talk). CSL Dale Miller, Jui-Hsuan Wu
2023	A*	`conf`	A system of inference based on proof search: an extended abstract. LICS Dale Miller
2023	J	`jnl`	A system of inference based on proof search: an extended abstract. CoRR Dale Miller
2023	—	`conf`	Formal Reasoning Using Distributed Assertions. FroCoS Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller
2023	J	`jnl`	Peano Arithmetic and μMALL. CoRR Matteo Manighetti, Dale Miller
2022	J	`jnl`	A Survey of the Proof-Theoretic Foundations of Logic Programming. Theory Pract. Log. Program. Dale Miller
2022	J	`jnl`	From axioms to synthetic inference rules via focusing. Ann. Pure Appl. Log. Sonia Marin, Dale Miller, Elaine Pimentel, Marco Volpe
2022	J	`jnl`	Functions-as-constructors higher-order unification: extended pattern unification. Ann. Math. Artif. Intell. Tomer Libal, Dale Miller
2022	J	`jnl`	The undecidability of proof search when equality is a logical connective. Ann. Math. Artif. Intell. Dale Miller, Alexandre Viel
2021	J	`jnl`	A Survey of the Proof-Theoretic Foundations of Logic Programming. CoRR Dale Miller
2020	Misc	`conf`	A Distributed and Trusted Web of Formal Proofs. ICDCIT Dale Miller
2020	—	`conf`	Andre and the Early Days of Penn's Logic and Computation Group. Logic, Language, and Security Dale Miller
2020	J	`jnl`	EATCS Distinguished Dissertation Award 2020 - Call for Nominations. Bull. EATCS Susanne Albers, Nikhil Bansal, Elvira Mayordomo, Dale Miller, Jaroslav Nesetril, Damian Niwinski, David Peleg, Vladimiro Sassone, Alexandra Silva
2020	B	`conf`	Extrinsically typed operational semantics for functional languages. SLE Matteo Cimini, Dale Miller, Jeremy G. Siek
2020	A*	`ed.`	LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020. LICS Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller
2020	—	`conf`	Two Applications of Logic Programming to Coq. TYPES Matteo Manighetti, Dale Miller, Alberto Momigliano
2019	J	`jnl`	A Proof Theory for Model Checking. J. Autom. Reason. Quentin Heath, Dale Miller
2019	B	`conf`	A proof-theoretic approach to certifying skolemization. CPP Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller
2019	J	`jnl`	EATCS Distinguished Dissertation Award 2019 - Call for Nominations. Bull. EATCS David Peleg, Susanne Albers, Elvira Mayordomo, Dale Miller, Jaroslav Nesetril, Damian Niwinski, Vladimiro Sassone
2019	J	`jnl`	Functional programming with lambda-tree syntax. CoRR Ulysse Gérard, Dale Miller, Gabriel Scherer
2019	C	`conf`	Functional programming with λ-tree syntax. PPDP Ulysse Gérard, Dale Miller, Gabriel Scherer
2019	J	`jnl`	Mechanized Metatheory Revisited. J. Autom. Reason. Dale Miller
2019	—	`ed.`	Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019. LFMTP@LICS Dale Miller, Ivan Scagnetto
2019	C	`conf`	Property-Based Testing via Proof Reconstruction. PPDP Roberto Blanco, Dale Miller, Alberto Momigliano
2017	B	`ed.`	2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, Oxford, UK, September 3-9, 2017 FSCD Dale Miller
2017	J	`jnl`	A Semantic Framework for Proof Evidence. J. Autom. Reason. Zakaria Chihani, Dale Miller, Fabien Renaud
2017	J	`jnl`	Proof checking and logic programming. Formal Aspects Comput. Dale Miller
2017	B	`conf`	Separating Functional Computation from Relations. CSL Ulysse Gérard, Dale Miller
2017	A	`conf`	Translating Between Implicit and Explicit Versions of Proof. CADE Roberto Blanco, Zakaria Chihani, Dale Miller
2016	—	`conf`	A Proof Theory for Model Checking: An Extended Abstract. LINEARITY Quentin Heath, Dale Miller
2016	B	`conf`	A focused framework for emulating modal proof systems. Advances in Modal Logic Sonia Marin, Dale Miller, Marco Volpe
2016	J	`jnl`	A multi-focused proof system isomorphic to expansion proofs. J. Log. Comput. Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller
2016	B	`conf`	Functions-as-Constructors Higher-Order Unification. FSCD Tomer Libal, Dale Miller
2016	—	`conf`	Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). TYPES Dale Miller
2016	J	`jnl`	Preserving differential privacy under finite-precision semantics. Theor. Comput. Sci. Ivan Gazeau, Dale Miller, Catuscia Palamidessi
2016	J	`jnl`	Well-Typed Languages are Sound. CoRR Matteo Cimini, Dale Miller, Jeremy G. Siek
2015	B	`conf`	A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. CPP Kaustuv Chaudhuri, Matteo Cimini, Dale Miller
2015	—	`conf`	A framework for proof certificates in finite state exploration. PxTP@CADE Quentin Heath, Dale Miller
2015	—	`conf`	Defining the meaning of TPTP formatted proofs. IWIL@LPAR Roberto Blanco, Tomer Libal, Dale Miller
2015	B	`conf`	Focused Labeled Proof Systems for Modal Logic. LPAR Dale Miller, Marco Volpe
2015	B	`conf`	On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control. LPAR Chuck C. Liang, Dale Miller
2015	—	`conf`	Proof Certificates for Equality Reasoning. LSFA Zakaria Chihani, Dale Miller
2015	C	`conf`	Proof Checking and Logic Programming. LOPSTR Dale Miller
2015	—	`conf`	Proof Outlines as Proof Certificates: A System Description. WoF'15 Roberto Blanco, Dale Miller
2015	C	`conf`	Proof checking and logic programming. PPDP Dale Miller
2014	J	`jnl`	Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
2014	—	`ch.`	Automation of Higher-Order Logic. Computational Logic Christoph Benzmüller, Dale Miller
2014	—	`ed.`	Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, July 14 - 18, 2014 CSL-LICS Thomas A. Henzinger, Dale Miller
2013	J	`jnl`	A formal framework for specifying sequent calculus proof systems. Theor. Comput. Sci. Dale Miller, Elaine Pimentel
2013	—	`conf`	Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). PxTP@CADE Zakaria Chihani, Dale Miller, Fabien Renaud
2013	B	`conf`	Extracting Proofs from Tabled Proof Search. CPP Dale Miller, Alwen Tiu
2013	A	`conf`	Foundational Proof Certificates in First-Order Logic. CADE Zakaria Chihani, Dale Miller, Fabien Renaud
2013	—	`conf`	Foundational proof certificates: making proof universal and permanent. LFMTP Dale Miller
2013	J	`jnl`	Kripke semantics and proof systems for combining intuitionistic logic and classical logic. Ann. Pure Appl. Log. Chuck C. Liang, Dale Miller
2013	—	`conf`	Preserving differential privacy under finite-precision semantics. QAPL Ivan Gazeau, Dale Miller, Catuscia Palamidessi
2013	A*	`conf`	Unifying Classical and Intuitionistic Logics for Computational Control. LICS Chuck C. Liang, Dale Miller
2012	B	`conf`	A Systematic Approach to Canonicity in the Classical Sequent Calculus. CSL Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller
2012	J	`jnl`	A Two-Level Logic Approach to Reasoning About Computations. J. Autom. Reason. Andrew Gacek, Dale Miller, Gopalan Nadathur
2012	—	`conf`	A non-local method for robustness analysis of floating point programs QAPL Ivan Gazeau, Dale Miller, Catuscia Palamidessi
2012	A	`ed.`	Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings IJCAR Bernhard Gramlich, Dale Miller, Uli Sattler
2012	B	`ed.`	Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings CPP Chris Hawblitzel, Dale Miller
2012	—	`ed.`	Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, Tallinn, Estonia, 24th March 2012. FICS Dale Miller, Zoltán Ésik
2012	—	`book`	Programming with Higher-Order Logic. Dale Miller, Gopalan Nadathur
2011	B	`conf`	A Proposal for Broad Spectrum Proof Certificates. CPP Dale Miller
2011	J	`jnl`	A focused approach to combining logics. Ann. Pure Appl. Log. Chuck C. Liang, Dale Miller
2011	J	`jnl`	Nominal abstraction. Inf. Comput. Andrew Gacek, Dale Miller, Gopalan Nadathur
2010	J	`jnl`	A Framework for Proof Systems. J. Autom. Reason. Vivek Nigam, Dale Miller
2010	—	`conf`	Fixed Points and Proof Theory: An Extended Abstract. FICS Dale Miller
2010	A	`conf`	Focused Inductive Theorem Proving. IJCAR David Baelde, Dale Miller, Zachary Snow
2010	J	`jnl`	Proof and refutation in MALL as a game. Ann. Pure Appl. Log. Olivier Delande, Dale Miller, Alexis Saurin
2010	J	`jnl`	Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log. Alwen Tiu, Dale Miller
2010	B	`conf`	Reasoning about Computations Using Two-Levels of Logic. APLAS Dale Miller
2009	A*	`conf`	A Unified Sequent Calculus for Focused Proofs. LICS Chuck C. Liang, Dale Miller
2009	J	`jnl`	A two-level logic approach to reasoning about computations CoRR Andrew Gacek, Dale Miller, Gopalan Nadathur
2009	C	`conf`	Algorithmic specifications in linear logic with subexponentials. PPDP Vivek Nigam, Dale Miller
2009	J	`jnl`	Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. Chuck C. Liang, Dale Miller
2009	J	`jnl`	Nominal Abstraction CoRR Andrew Gacek, Dale Miller, Gopalan Nadathur
2008	A*	`conf`	A Neutral Approach to Proof and Refutation in MALL. LICS Olivier Delande, Dale Miller
2008	—	`conf`	Canonical Sequent Proofs via Multi-Focusing. IFIP TCS Kaustuv Chaudhuri, Dale Miller, Alexis Saurin
2008	A*	`conf`	Combining Generic Judgments with Recursive Definitions. LICS Andrew Gacek, Dale Miller, Gopalan Nadathur
2008	J	`jnl`	Combining generic judgments with recursive definitions CoRR Andrew Gacek, Dale Miller, Gopalan Nadathur
2008	A	`conf`	Focusing in Linear Meta-logic. IJCAR Vivek Nigam, Dale Miller
2008	J	`jnl`	Formalizing Operational Semantic Specifications in Logic. Bull. EATCS Dale Miller
2008	—	`conf`	Formalizing Operational Semantic Specifications in Logic. WFLP Dale Miller
2008	J	`jnl`	Proof Search Specifications for Bisimulation and Modal Logics for the pi-Calculus CoRR Alwen Tiu, Dale Miller
2008	J	`jnl`	Reasoning in Abella about Structural Operational Semantics Specifications CoRR Andrew Gacek, Dale Miller, Gopalan Nadathur
2008	—	`conf`	Reasoning in Abella about Structural Operational Semantics Specifications. LFMTP@LICS Andrew Gacek, Dale Miller, Gopalan Nadathur
2007	J	`jnl`	Collection analysis for Horn clause programs CoRR Dale Miller
2007	J	`jnl`	Focusing and Polarization in Intuitionistic Logic CoRR Chuck C. Liang, Dale Miller
2007	B	`conf`	Focusing and Polarization in Intuitionistic Logic. CSL Chuck C. Liang, Dale Miller
2007	B	`conf`	From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic. CSL Dale Miller, Alexis Saurin
2007	B	`conf`	Incorporating Tables into Proofs. CSL Dale Miller, Vivek Nigam
2007	B	`conf`	Least and Greatest Fixed Points in Linear Logic. LPAR David Baelde, Dale Miller
2007	A	`conf`	The Bedwyr System for Model Checking over Syntactic Expressions. CADE David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
2007	J	`jnl`	The Bedwyr system for model checking over syntactic expressions CoRR David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
2006	C	`conf`	Collection analysis for Horn clause programs. PPDP Dale Miller
2006	A	`conf`	Representing and Reasoning with Operational Semantics. IJCAR Dale Miller
2006	B	`conf`	Roadmap for enhanced languages and methods to aid verification. GPCE Gary T. Leavens, Jean-Raymond Abrial, Don S. Batory, Michael J. Butler, Alessandro Coglio, Kathi Fisler, Eric C. R. Hehner, Cliff B. Jones, Dale Miller, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump
2005	—	`conf`	A Congruence Format for Name-passing Calculi. SOS@ICALP Axelle Ziegler, Dale Miller, Catuscia Palamidessi
2005	B	`conf`	A Game Semantics for Proof Search: Preliminary Results. MFPS Dale Miller, Alexis Saurin
2005	—	`conf`	A Proof Theoretic Approach to Operational Semantics. APC 25 Dale Miller
2005	—	`conf`	A game semantics for proof search: preliminary results. GALOP@ETAPS Dale Miller, Alexis Saurin
2005	J	`jnl`	A proof theory for generic judgments. ACM Trans. Comput. Log. Dale Miller, Alwen Tiu
2005	B	`conf`	On the Specification of Sequent Systems. LPAR Elaine Pimentel, Dale Miller
2004	—	`conf`	A Proof Search Specification of the pi-Calculus. FGUC Alwen Fernanto Tiu, Dale Miller
2004	B	`conf`	Bindings, Mobility of Bindings, and the "generic judgments"-Quantifier: An Abstract. CSL Dale Miller
2003	A*	`conf`	A Proof Theory for Generic Judgments: An extended abstract. LICS Dale Miller, Alwen Fernanto Tiu
2003	J	`jnl`	Encoding transition systems in sequent calculus. Theor. Comput. Sci. Raymond McDowell, Dale Miller, Catuscia Palamidessi
2003	C	`conf`	Encryption as an abstract data type. WoLLIC Dale Miller
2003	—	`conf`	Reasoning about Proof Search Specifications: An Abstract. TPHOLs Dale Miller
2002	—	`conf`	Encoding Generic Judgments. FSTTCS Dale Miller, Alwen Fernanto Tiu
2002	—	`conf`	Higher-Order Quantification and Proof Search. AMAST Dale Miller
2002	J	`jnl`	Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log. Raymond McDowell, Dale Miller
2002	B	`conf`	Using Linear Logic to Reason about Sequent Systems. TABLEAUX Dale Miller, Elaine Pimentel
2001	—	`conf`	Encoding Generic Judgments: Preliminary results. MERLIN Dale Miller
2000	—	`conf`	Abstract Syntax for Variable Binders: An Overview. Computational Logic Dale Miller
2000	J	`jnl`	Cut-elimination for a logic with definitions and induction. Theor. Comput. Sci. Raymond McDowell, Dale Miller
2000	J	`jnl`	Reasoning with Higher-Order Abstract Syntax in a Logical Framework CoRR Raymond McDowell, Dale Miller
1999	J	`jnl`	Foundational Aspects of Syntax. ACM Comput. Surv. Dale Miller, Catuscia Palamidessi
1997	A*	`conf`	A Logic for Reasoning with Higher-Order Abstract Syntax. LICS Raymond McDowell, Dale Miller
1996	—	`conf`	Encoding Transition Systems in Sequent Calculus. Linear Logic Tokyo Meeting Raymond McDowell, Dale Miller, Catuscia Palamidessi
1996	J	`jnl`	Forum: A Multiple-Conclusion Specification Logic. Theor. Comput. Sci. Dale Miller
1996	—	`conf`	Linear Logic as Logic Programming: An Abstract. LACL Dale Miller
1996	J	`jnl`	Logical Foundations for Open System Design. ACM Comput. Surv. Dale Miller
1995	—	`ch.`	Annotations are not "for free": The Need for Runtime Layer Support in Hypertext Engines. Designing User Interfaces for Hypermedia Christine M. Neuwirth, Ravinder Chandhok, David Kaufer, James H. Morris, Paul Erion, Dale Miller
1995	—	`conf`	Observations about Using Logic as a Specification Language. GULP-PRODE Dale Miller
1994	A*	`conf`	A Multiple-Conclusion Meta-Logic LICS Dale Miller
1994	J	`jnl`	Logic Programming in a Fragment of Intuitionistic Linear Logic Inf. Comput. Joshua S. Hodas, Dale Miller
1994	—	`conf`	Specifications Using Multiple-Conclusion Logic Programs. ALP Dale Miller
1994	—	`conf`	Specifications Using Multiple-Conclusion Logic Programs. PLILP Dale Miller
1993	—	`conf`	A Proposal for Modules in Lambda-Prolog. ELP Dale Miller
1993	—	`ed.`	Logic Programming, Proceedings of the 1993 International Symposium, Vancouver, British Columbia, Canada, October 26-29, 1993 ILPS Dale Miller
1992	A	`conf`	Flexible Diff-ing in a Collaborative Writing System. CSCW Christine Neuwirth, Ravinder Chandhok, David Kaufer, Paul Erion, James H. Morris, Dale Miller
1992	J	`jnl`	From Operational Semantics for Abstract Machines. Math. Struct. Comput. Sci. John Hannan, Dale Miller
1992	—	`conf`	The pi-Calculus as a Theory in Linear Logic: Preliminary Results. ELP Dale Miller
1992	J	`jnl`	Unification Under a Mixed Prefix. J. Symb. Comput. Dale Miller
1991	J	`jnl`	A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. J. Log. Comput. Dale Miller
1991	—	`conf`	Abstract Syntax and Logic Programming. RCLP Dale Miller
1991	A*	`conf`	Logic Programming in a Fragment of Intuitionistic Linear Logic LICS Joshua S. Hodas, Dale Miller
1991	B	`conf`	Logics for Logic Programming: A Tutorial. ICLP Dale Miller
1991	B	`conf`	Unification of Simply Typed Lamda-Terms as Logic Programming. ICLP Dale Miller
1991	J	`jnl`	Uniform Proofs as a Foundation for Logic Programming. Ann. Pure Appl. Log. Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov
1990	A	`conf`	Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. CADE Amy P. Felty, Dale Miller
1990	B	`conf`	Extending Definite Clause Grammars with Scoping Constructs. ICLP Remo Pareschi, Dale Miller
1990	—	`conf`	From Operational Semantics to Abstract Machines: Preliminary Results. LISP and Functional Programming John Hannan, Dale Miller
1990	J	`jnl`	Higher-Order Horn Clauses J. ACM Gopalan Nadathur, Dale Miller
1990	B	`conf`	Higher-Order Logic Programming. ICLP Dale Miller
1990	B	`conf`	Representing Objects in a Logic Programming Langueage with Scoping Constructs. ICLP Joshua S. Hodas, Dale Miller
1990	A	`conf`	Tutorial on Lambda-Prolog. CADE Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning
1989	—	`conf`	A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. ELP Dale Miller
1989	J	`jnl`	A Logical Analysis of Modules in Logic Programming. J. Log. Program. Dale Miller
1989	B	`conf`	Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language. MPC John Hannan, Dale Miller
1989	B	`conf`	Lexical Scoping as Universal Quantification. ICLP Dale Miller
1988	—	`conf`	A Meta-Logic for Functional Programming. META John Hannan, Dale Miller
1988	—	`conf`	An Overview of Lambda-PROLOG. ICLP/SLP Gopalan Nadathur, Dale Miller
1988	A	`conf`	Lambda-Prolog: An Extended Logic Programming Language. CADE Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov
1988	A	`conf`	Specifying Theorem Provers in a Higher-Order Logic Programming Language. CADE Amy P. Felty, Dale Miller
1988	—	`conf`	Uses of Higher-Order Unification for Implementing Program Transformers. ICLP/SLP John Hannan, Dale Miller
1987	—	`conf`	A Logic Programming Approach to Manipulating Formulas and Programs. SLP Dale Miller, Gopalan Nadathur
1987	A*	`conf`	Hereditary Harrop Formulas and Uniform Proof Systems LICS Dale Miller, Gopalan Nadathur, Andre Scedrov
1986	—	`conf`	A Theory of Modules for Logic Programming. SLP Dale Miller
1986	A*	`conf`	An Integration of Resolution and Natural Deduction Theorem Proving. AAAI Dale Miller, Amy P. Felty
1986	B	`conf`	Higher-Order Logic Programming. ICLP Dale Miller, Gopalan Nadathur
1986	—	`conf`	Research in Natural Language Processing. HLT Aravind K. Joshi, Timothy W. Finin, Dale Miller, Lokendra Shastri, Bonnie L. Webber
1986	A*	`conf`	Some Uses of Higher-Order Logic in Computational Linguistics. ACL Dale Miller, Gopalan Nadathur
1984	A	`conf`	Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. CADE Dale Miller