Currículo do Sistema de Currículos Lattes (Dale Miller)

Curriculum Vitae
Dale Miller

Última atualização em 09/03/2006

Dados Pessoais

Nome Dale Miller
Nascimento 11/12/1956 - Estados Unidos
Carteira de Identidade - -
CPF
Passaporte ----------

Formação Acadêmica/Titulação

1991 - 1991 Pós-Doutorado.
University of Glasgow, U.GLASGOW, Glasgow, Escócia
1990 - 1991 Pós-Doutorado.
University of Edinburgh, EDINBURGH, Edinburgh, Escócia
1994 - 1994 Pós-Doutorado.
Universita degli Studi - Pisa, U.D.S.P., Pisa, Itália
1996 - 1996 Pós-Doutorado.
Universita Degli Studi Genova, UNIGEN, Itália
1997 - 1997 Pós-Doutorado.
Universita degli Studi - Siena, SIENA, Siena, Itália
2002 - 2002 Pós-Doutorado.
Universite d'Aix-Marseille III (Droit, Econ. et Sciences), U.D.M. III, Aix-En-Provence, França
1978 - 1983 Doutorado em Mathematics.
Carnegie Mellon University, CARNEGIE MELLON, Pittsburgh, Estados Unidos
Título: L-calculus, Ano de obtenção: 1983
Orientador: Peter Andrews
1974 - 1978 Graduação em B S Mathematics.
Lebanon Valley College, LVC, Estados Unidos

Início da página

Atuação Profissional

1 Carnegie Mellon University - CARNEGIE MELLON

Vínculo institucional
1978 - 1983 Vínculo: Outro , Enquadramento funcional: Research Assistant , Carga horária: 40, Regime : Dedicação Exclusiva

Atividades
/1978 - /1983
Pesquisa e Desenvolvimento, Department Of Mathematics

Linhas de Pesquisa
1. Mathematics

2 École Polytechnique - POLYTECHNIQUE

Vínculo institucional
2002 - Vínculo: Outro , Enquadramento funcional: Professor titular , Carga horária: 20, Regime : Parcial

Atividades
/2002 - Atual
Pós-graduação

1. Logic and Computer Science

/2002 - Atual Pesquisa e Desenvolvimento, Lix

Linhas de Pesquisa
1. Logic and Computer Science

3 Institut National de Recherche En Informatique Et En Automatique - INRIA

Vínculo institucional
2002 - Vínculo: Outro , Enquadramento funcional: Directeur de Recherche , Carga horária: 0, Regime : Dedicação Exclusiva

Atividades
/2002 - Atual
Pesquisa e Desenvolvimento, Futurs

Linhas de Pesquisa
1. Logic and Computer Science

/2002 - Atual Direção e Administração, Futurs

Cargos Ocupados
1. Directeur de Recherche

4 National Institute of Standards and Technology - NIST

Vínculo institucional
1977 - 1978 Vínculo: Outro , Enquadramento funcional: Mathematician , Carga horária: 40, Regime : Dedicação Exclusiva

Atividades
/1977 - /1978
Pesquisa e Desenvolvimento, Ai Lab

Linhas de Pesquisa
1. Mathematics

5 The Pennsylvania State University - PENNSTATE

Vínculo institucional
1997 - 2002 Vínculo: Outro , Enquadramento funcional: Professor titular , Carga horária: 40, Regime : Dedicação Exclusiva

Atividades
/1997 - /2001
Direção e Administração, Computer Science Department, Cse

Cargos Ocupados
1. Head

/1997 - /2002 Pós-graduação

1. Semantics of Programming Languages
2. Type theory
3. Logic and Computer Science

/1997 - /2002 Pesquisa e Desenvolvimento, Computer Science Department

Linhas de Pesquisa
1. Logic and Computer Science

6 University of Pennsylvania - U.P.

Vínculo institucional
1983 - 1997 Vínculo: Outro , Enquadramento funcional: Professor titular , Carga horária: 40, Regime : Dedicação Exclusiva

Atividades
/1983 - /1997
Pós-graduação

1. Logic and Computer Science
2. Type theory
3. Semantics of Programming Languages

/1983 - /1997 Pesquisa e Desenvolvimento, Department Of Computer Science

Linhas de Pesquisa
1. Logic and Computer Science

Início da página

Áreas de atuação

1 Lógicas e Semântica de Programas
2 Lógica Matemática

Início da página

Idiomas

Entende Inglês (Bem) , Italiano (Bem) , Francês (Bem)
Fala Inglês (Bem) , Italiano (Bem) , Francês (Bem)
Lê Inglês (Bem) , Italiano (Bem) , Francês (Bem)
Escreve Inglês (Bem) , Italiano (Bem) , Francês (Bem)

Início da página

Produção científica, tecnológica e artística/cultural

Produção bibliográfica Produção técnica Produção artística/cultural

Artigos completos publicados em periódicos

1 MILLER, D.
Logic and Logic Programming: a personal account. Newsletter of the Association for Logic Programming. , v.16, n.1, 2006.
2 MILLER, D., TIU, A.
A Proof Theory for Generic Judgments. ACM Transactions on Computational Logic. , v.6, n.4, p.749 - 783, 2005.
3 MILLER, D., PALAMIDESSI, C., MCDOWELL, R.
Encoding Transition Systems in Sequent Calculus. Theoretical Computer Science. , v.294, n.3, p.411 - 437, 2003.
4 MILLER, D., MCDOWELL, R.
Reasoning with Higher-Order Abstract Syntax in a Logical Framework. Acm Transaction On Computational Logic. , v.3, n.1, p.80 - 136, 2002.
5 MILLER, D., MCDOWELL, R.
Cut-Elimination for a Logic with Definitions and Induction. Theoretical Computer Science. , v.232, p.91 - 119, 2000.
6 MILLER, D., PALAMIDESSI, C.
Foundational Aspects of Syntax. ACM Computing Surveys. , v.31, n.3, 1999.
7 MILLER, D.
Forum: A multiple-conclusion specification logic. Theoretical Computer Science. , v.165, n.1, p.201 - 232, 1996.
8 MILLER, D., HODAS, J.
Logic programming in a fragment of intuitionistic linear logic. Information And Computation. , v.110, n.2, p.327 - 365, 1994.
9 MILLER, D., HANNAN, J.
From operational semantics to abstract machines. Mathematical Structures In Computer Science. , v.2, n.4, p.415 - 459, 1992.
10 MILLER, D.
Unification under a mixed prefix. Journal of Symbolic Computation. , v.14, p.321 - 358, 1992.
11 MILLER, D.
A logic programming language with lambda-abstraction, function variables, and simple unification. Journal Of Logic And Computation. , v.1, n.4, p.497 - 536, 1991.
12 MILLER, D., NADATHUR, G., PFENNING, F., SCEDROV, A.
Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic. , v.51, p.125 - 157, 1991.
13 MILLER, D., NADATHUR, G.
Higher-order Horn clauses. Journal Of The ACM. , v.37, n.4, p.777 - 814, 1990.
14 MILLER, D.
A logical analysis of modules in logic programming. Journal of Logic Programming. , v.6, p.79 - 108, 1989.
15 MILLER, D.
A compact representation of proofs. Studia Logica. , v.46, n.4, p.345 - 368, 1987.

Início da página

Livros publicados

1 MILLER, D., NADATHUR, G.
lProlog: An Introduction to the Language and its Logic, 2003

Capítulos de livros publicados

1 MILLER, D., PIMENTEL, E. G.
Linear logic as a framework for specifying sequent calculus In: Lecture Notes in Logic ed.Illinois : Association for symbolic logic, 2004, v.17, p. 111-135.
2 MILLER, D.
Overview of linear logic programming In: Linear Logic in Computer Science ed. : Cambridge University Press, 2004, v.316, p. 119-150.
3 MILLER, D., NADATHUR, G.
Higher-order Logic Programming In: Handbook of Logic in Artificial Intelligence and Logic Programming ed.Oxford : Clarendon Press, 1998, p. 499-590.
4 MILLER, D.
Logic Programming and Meta-Logic In: The Logic of Computation ed. : Springer-Verlag, 1997, p. 265-308.
5 MILLER, D.
Sequent Calculus and the Specification of Computation In: Computational Logic ed. : Springer, 1997
6 MILLER, D.
Abstractions in logic programming In: Logic and Computer Science ed. : Academic Press, 1990, p. 329-359.
7 MILLER, D., HANNAN, J.
A Meta-Language for Functional Programming In: Meta-Programming in Logic Programming ed. : MIT Press, 1989, p. 453-476.
8 MILLER, D., ANDREWS, P. B., COHEN, E. L., PFENNING, F.
Automating higher order logic In: Automated Theorem Proving: After 25 Years ed. : AMS, 1984, p. 169-192.

Início da página

Trabalhos completos publicados em anais de evento

1 MILLER, D., PALAMIDESSI, C., ZIEGLER, A.
A congruence format for name-passing calculi In: Structural Operational Semantics, 2005, Lisboa.
  Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
2 MILLER, D., SAURIN, A.
A game semantics for proof search: Preliminary results In: Mathematical Foundations of Programming Semantics, 2005, Birmingham.
  Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
3 MILLER, D.
A Proof Theoretic Approach to Operational Semantics In: Algebraic Process Calculi: The First Twenty Five Years and Beyond, 2005, Bertinoro.
  Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
4 MILLER, D., TIU, A., NADATHUR, G.
Mixing Finite Success and Finite Failure in an Automated Prover In: ESHOL'05: Empirically Successful Automated Reasoning in Higher-Order Logics, 2005, Montego Bay.
  Proceedings of ESHOL. , 2005.
5 MILLER, D., PIMENTEL, E. G.
On the specification of sequent systems In: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2005, Montego Bay.
  LNAI. Springer, 2005. v.3835. p.352 - 366
6 MILLER, D., TIU, A.
A Proof Search Specification of the Pi-Calculus In: Workshop on the Foundations of Global Ubiquitous Computing, 2004, Londres.
  Electronic Notes in Theoretical Computer Science. Elsevier, 2004. v.184. p.79 - 101
7 MILLER, D., TIU, A.
A Proof Theory for Generic Judgments: An extended abstract In: LICS, 2003, Ottawa.
  Proceedings IEEE Computer Society 2003. IEEE Computer Society, 2003. p.118 - 127
8 MILLER, D.
Encryption as an abstract data-type: An extended abstract In: Foundations of Computer Security, 2003, Stanford.
  Electronic Notes in Theoretical Computer Science. Elsevier, 2003. v.84. p.1 - 12
9 MILLER, D., TIU, A.
Encoding Generic Judgments In: 22nd Foundations of Software Technology and Theoretical Computer Science
  . , 2002.
10 MILLER, D.
Higher-order quantification and proof search In: AMAST 2002
  LNCS. , 2002. v.2422. p.60 - 74
11 MILLER, D., PIMENTEL, E. G.
Using linear logic to reason about sequent systems In: Tableaux 2002
  LNCS. , 2002.
12 MILLER, D.
Encoding generic judgments: Preliminary results In: Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001)
  Electronic Notes of TCS. , 2001.
13 MILLER, D.
Abstract Syntax for Variable Binders: An Overview In: Computational Logic - CL2000
  LNAI. , 2000. v.1861.
14 MILLER, D., MCDOWELL, R.
A Logic for Reasoning with Higher-Order Abstract Syntax In: Symposium on Logics in Computer Science
  . , 1997.
15 MILLER, D., PALAMIDESSI, C., MCDOWELL, R.
Encoding Transition Systems in Sequent Calculus: Preliminary Report In: Linear Logic Workshop
  . , 1996.
16 MILLER, D.
Logical Foundations for Open System Design In: Computing Surveys
  . , 1996.
17 MILLER, D.
A Multiple-Conclusion Meta-Logic In: 1994 Symposium on Logics in Computer Science
  . , 1994.
18 MILLER, D.
The p-calculus as a theory in linear logic: Preliminary results In: 1992 Workshop on Extensions to Logic Programming
  . , 1992.
19 MILLER, D., HODAS, J.
Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract In: Logics in Computer Science
  . , 1991.
20 MILLER, D.
Unification of Simply Typed Lambda-Terms as Logic Programming In: 1991 International Conference on Logic programming
  . , 1991.
21 MILLER, D., FELTY, A.
Encoding a Dependent-Type l-Calculus in a Logic Programming Language In: 1990 Conference on Automated Deduction
  . , 1990.
22 MILLER, D., PARESCHI, R.
Extending Definite Clause Grammars with Scoping Constructs In: 1990 International Conference in Logic Programming
  . , 1990.
23 MILLER, D., HANNAN, J.
From Operational Semantics to Abstract Machines: Preliminary Results In: 1990 LISP and Functional Programming Conference
  . , 1990.
24 MILLER, D., HODAS, J.
Representing Objects in a Logic Programming Language with Scoping Constructs In: 1990 International Conference in Logic Programming
  . , 1990.
25 MILLER, D.
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification In: Extentions of Logic Programming
  . , 1989.
26 MILLER, D.
Lexical Scoping as Universal Quantification In: Sixth International Logic Programming Conference
  . , 1989.
27 MILLER, D., NADATHUR, G.
An overview of lProlog In: Fifth Symposium on Logic Programming
  . , 1988.
28 MILLER, D., FELTY, A.
Specifying theorem provers in a higher-order logic programming language In: 9th International Conference on Automated Deduction
  . , 1988.
29 MILLER, D., HANNAN, J.
Uses of higher-order unification for implementing program transformers In: Fifth Symposium on Logic Programming
  . , 1988.
30 MILLER, D., NADATHUR, G.
A logic programming approach to manipulating formulas and programs In: IEEE Symposium on Logic Programming
  . , 1987.
31 MILLER, D., NADATHUR, G., SCEDROV, A.
Hereditary Harrop formulas and uniform proofs systems In: Second Anual Symposium on Logic in Computer Science
  . , 1987.
32 MILLER, D.
A theory of modules for logic programming In: IEEE Symposium on Logic Programming
  . , 1986.
33 MILLER, D., FELTY, A.
An integration of resolution and natural deduction theorem proving In: National Conference on Artificial Intelligence
  . , 1986.
34 MILLER, D., NADATHUR, G.
Higher-order logic programming In: Third International Logic Programming Conference
  . , 1986.
35 MILLER, D., NADATHUR, G.
Some uses of higher-order logic in computational linguistics In: 24th Annual Meeting of the Association for Computational Linguistics
  . , 1986.
36 MILLER, D.
Expansion tree proofs and their conversion to natural deduction proofs In: 7th Conference on Automated Deduction
  . , 1984.
37 MILLER, D., ANDREWS, P. B., COHEN, E. L.
A look at TPS In: 6th Conference on Automated Deduction
  . , 1982.

Início da página

Orientações concluídas

Dissertações de mestrado : orientador principal Orientações concluídas

1 Jeremie Wajs. Design and implementation of a theorem prover for operational semantics. 2000. Dissertação (Computer Science) - The Pennsylvania State University
2 Alexander Betis. Object Programming, Linear Logic and Java. 1999. Dissertação (Computer Science) - The Pennsylvania State University
3 Joshua Hodas. Object-Oriented Programming in Logic Programming. 1990. Dissertação (Computer Science) - University of Pennsylvania
4 Amy Felty. Using extended tactics to do proof transformations. 1986. Dissertação (Computer Science) - University of Pennsylvania
5 Greg Hager. Computational aspects of proofs in modal logic. 1985. Dissertação (Computer Science) - University of Pennsylvania

Teses de doutorado : orientador principal Orientações concluídas

1 Alwen Tiu. A Logical Framework for Reasoning about Logical Specifications. 2004. Tese (Theoretical Computer Science) - Ecole Polytechnique - Paris
2 Jeremie Wajs. Reasoning about logic programs using definitions and induction. 2002. Tese (Computer Science) - The Pennsylvania State University
3 Elaine Gouvêa Pimentel. Linear Logic and the specification of sequent systems. 2001. Tese (Ciência da Computação) - Universidade Federal de Minas Gerais
4 Raymond McDowell. Ray McDowell. 1997. Tese (Computer Science) - The Pennsylvania State University
5 Chuck Liang. Object-language substitution and unification in meta-logic. 1995. Tese (Computer Science) - University of Pennsylvania
6 Jawahar Chirimar. Proof Theoretic Approach To Specification Languages. 1995. Tese (Computer Science) - University of Pennsylvania
7 Joshua Hodas. Logic Programming in Intuitionistic Linear Logic: Theory, Design, and Implementation. 1993. Tese (Computer Science) - University of Pennsylvania
8 John Hannan. Proof-theoretic methods for analysis of functional programs. 1990. Tese (Computer Science) - University of Pennsylvania
9 Amy Felty. Implementing theorem provers in a higher-order logic programming language. 1989. Tese (Computer Science) - University of Pennsylvania
10 Gopalan Nadathur. A higher-order logic as the basis for logic programming. 1986. Tese (Computer Science) - University of Pennsylvania

Início da página

Indicadores de produção

Produção bibliográfica Produção técnica Produção artística/cultural Orientações concluídas Demais trabalhos

Informações complementares
Orientações em andamento 3
Produção bibliográfica
Artigos publicados em periódicos 15
Completos 15
Trabalhos publicados em anais de eventos 37
Completos 37
Livros ou capítulos de livros 9
Livros publicados 1
Capítulos de livros publicados 8
Orientação concluída
Dissertações de mestrado 5
Teses de doutorado 10

Nome	Dale Miller
Nascimento	11/12/1956 - Estados Unidos
Carteira de Identidade	- -
CPF
Passaporte	----------

1991 - 1991	Pós-Doutorado. University of Glasgow, U.GLASGOW, Glasgow, Escócia
1990 - 1991	Pós-Doutorado. University of Edinburgh, EDINBURGH, Edinburgh, Escócia
1994 - 1994	Pós-Doutorado. Universita degli Studi - Pisa, U.D.S.P., Pisa, Itália
1996 - 1996	Pós-Doutorado. Universita Degli Studi Genova, UNIGEN, Itália
1997 - 1997	Pós-Doutorado. Universita degli Studi - Siena, SIENA, Siena, Itália
2002 - 2002	Pós-Doutorado. Universite d'Aix-Marseille III (Droit, Econ. et Sciences), U.D.M. III, Aix-En-Provence, França
1978 - 1983	Doutorado em Mathematics. Carnegie Mellon University, CARNEGIE MELLON, Pittsburgh, Estados Unidos Título: L-calculus, Ano de obtenção: 1983 Orientador: Peter Andrews
1974 - 1978	Graduação em B S Mathematics. Lebanon Valley College, LVC, Estados Unidos

	Vínculo institucional
	1978 - 1983	Vínculo: Outro , Enquadramento funcional: Research Assistant , Carga horária: 40, Regime : Dedicação Exclusiva

	Atividades
	/1978 - /1983	Pesquisa e Desenvolvimento, Department Of Mathematics
		Linhas de Pesquisa 1. Mathematics

	Vínculo institucional
	2002 -	Vínculo: Outro , Enquadramento funcional: Professor titular , Carga horária: 20, Regime : Parcial

	Atividades
	/2002 - Atual	Pós-graduação
		1. Logic and Computer Science
	/2002 - Atual	Pesquisa e Desenvolvimento, Lix
		Linhas de Pesquisa 1. Logic and Computer Science

	Atividades
	/2002 - Atual	Pesquisa e Desenvolvimento, Futurs
		Linhas de Pesquisa 1. Logic and Computer Science
	/2002 - Atual	Direção e Administração, Futurs
		Cargos Ocupados 1. Directeur de Recherche

	Vínculo institucional
	1977 - 1978	Vínculo: Outro , Enquadramento funcional: Mathematician , Carga horária: 40, Regime : Dedicação Exclusiva

	Atividades
	/1977 - /1978	Pesquisa e Desenvolvimento, Ai Lab
		Linhas de Pesquisa 1. Mathematics

	Vínculo institucional
	1997 - 2002	Vínculo: Outro , Enquadramento funcional: Professor titular , Carga horária: 40, Regime : Dedicação Exclusiva

	Atividades
	/1997 - /2001	Direção e Administração, Computer Science Department, Cse
		Cargos Ocupados 1. Head
	/1997 - /2002	Pós-graduação
		1. Semantics of Programming Languages 2. Type theory 3. Logic and Computer Science
	/1997 - /2002	Pesquisa e Desenvolvimento, Computer Science Department
		Linhas de Pesquisa 1. Logic and Computer Science

	Vínculo institucional
	1983 - 1997	Vínculo: Outro , Enquadramento funcional: Professor titular , Carga horária: 40, Regime : Dedicação Exclusiva

	Atividades
	/1983 - /1997	Pós-graduação
		1. Logic and Computer Science 2. Type theory 3. Semantics of Programming Languages
	/1983 - /1997	Pesquisa e Desenvolvimento, Department Of Computer Science
		Linhas de Pesquisa 1. Logic and Computer Science

Entende	Inglês (Bem) , Italiano (Bem) , Francês (Bem)
Fala	Inglês (Bem) , Italiano (Bem) , Francês (Bem)
Lê	Inglês (Bem) , Italiano (Bem) , Francês (Bem)
Escreve	Inglês (Bem) , Italiano (Bem) , Francês (Bem)

1	MILLER, D. Logic and Logic Programming: a personal account. Newsletter of the Association for Logic Programming. , v.16, n.1, 2006.
2	MILLER, D., TIU, A. A Proof Theory for Generic Judgments. ACM Transactions on Computational Logic. , v.6, n.4, p.749 - 783, 2005.
3	MILLER, D., PALAMIDESSI, C., MCDOWELL, R. Encoding Transition Systems in Sequent Calculus. Theoretical Computer Science. , v.294, n.3, p.411 - 437, 2003.
4	MILLER, D., MCDOWELL, R. Reasoning with Higher-Order Abstract Syntax in a Logical Framework. Acm Transaction On Computational Logic. , v.3, n.1, p.80 - 136, 2002.
5	MILLER, D., MCDOWELL, R. Cut-Elimination for a Logic with Definitions and Induction. Theoretical Computer Science. , v.232, p.91 - 119, 2000.
6	MILLER, D., PALAMIDESSI, C. Foundational Aspects of Syntax. ACM Computing Surveys. , v.31, n.3, 1999.
7	MILLER, D. Forum: A multiple-conclusion specification logic. Theoretical Computer Science. , v.165, n.1, p.201 - 232, 1996.
8	MILLER, D., HODAS, J. Logic programming in a fragment of intuitionistic linear logic. Information And Computation. , v.110, n.2, p.327 - 365, 1994.
9	MILLER, D., HANNAN, J. From operational semantics to abstract machines. Mathematical Structures In Computer Science. , v.2, n.4, p.415 - 459, 1992.
10	MILLER, D. Unification under a mixed prefix. Journal of Symbolic Computation. , v.14, p.321 - 358, 1992.
11	MILLER, D. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal Of Logic And Computation. , v.1, n.4, p.497 - 536, 1991.
12	MILLER, D., NADATHUR, G., PFENNING, F., SCEDROV, A. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic. , v.51, p.125 - 157, 1991.
13	MILLER, D., NADATHUR, G. Higher-order Horn clauses. Journal Of The ACM. , v.37, n.4, p.777 - 814, 1990.
14	MILLER, D. A logical analysis of modules in logic programming. Journal of Logic Programming. , v.6, p.79 - 108, 1989.
15	MILLER, D. A compact representation of proofs. Studia Logica. , v.46, n.4, p.345 - 368, 1987.

1	MILLER, D., PIMENTEL, E. G. Linear logic as a framework for specifying sequent calculus In: Lecture Notes in Logic ed.Illinois : Association for symbolic logic, 2004, v.17, p. 111-135.
2	MILLER, D. Overview of linear logic programming In: Linear Logic in Computer Science ed. : Cambridge University Press, 2004, v.316, p. 119-150.
3	MILLER, D., NADATHUR, G. Higher-order Logic Programming In: Handbook of Logic in Artificial Intelligence and Logic Programming ed.Oxford : Clarendon Press, 1998, p. 499-590.
4	MILLER, D. Logic Programming and Meta-Logic In: The Logic of Computation ed. : Springer-Verlag, 1997, p. 265-308.
5	MILLER, D. Sequent Calculus and the Specification of Computation In: Computational Logic ed. : Springer, 1997
6	MILLER, D. Abstractions in logic programming In: Logic and Computer Science ed. : Academic Press, 1990, p. 329-359.
7	MILLER, D., HANNAN, J. A Meta-Language for Functional Programming In: Meta-Programming in Logic Programming ed. : MIT Press, 1989, p. 453-476.
8	MILLER, D., ANDREWS, P. B., COHEN, E. L., PFENNING, F. Automating higher order logic In: Automated Theorem Proving: After 25 Years ed. : AMS, 1984, p. 169-192.

1	MILLER, D., PALAMIDESSI, C., ZIEGLER, A. A congruence format for name-passing calculi In: Structural Operational Semantics, 2005, Lisboa. Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
2	MILLER, D., SAURIN, A. A game semantics for proof search: Preliminary results In: Mathematical Foundations of Programming Semantics, 2005, Birmingham. Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
3	MILLER, D. A Proof Theoretic Approach to Operational Semantics In: Algebraic Process Calculi: The First Twenty Five Years and Beyond, 2005, Bertinoro. Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
4	MILLER, D., TIU, A., NADATHUR, G. Mixing Finite Success and Finite Failure in an Automated Prover In: ESHOL'05: Empirically Successful Automated Reasoning in Higher-Order Logics, 2005, Montego Bay. Proceedings of ESHOL. , 2005.
5	MILLER, D., PIMENTEL, E. G. On the specification of sequent systems In: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2005, Montego Bay. LNAI. Springer, 2005. v.3835. p.352 - 366
6	MILLER, D., TIU, A. A Proof Search Specification of the Pi-Calculus In: Workshop on the Foundations of Global Ubiquitous Computing, 2004, Londres. Electronic Notes in Theoretical Computer Science. Elsevier, 2004. v.184. p.79 - 101
7	MILLER, D., TIU, A. A Proof Theory for Generic Judgments: An extended abstract In: LICS, 2003, Ottawa. Proceedings IEEE Computer Society 2003. IEEE Computer Society, 2003. p.118 - 127
8	MILLER, D. Encryption as an abstract data-type: An extended abstract In: Foundations of Computer Security, 2003, Stanford. Electronic Notes in Theoretical Computer Science. Elsevier, 2003. v.84. p.1 - 12
9	MILLER, D., TIU, A. Encoding Generic Judgments In: 22nd Foundations of Software Technology and Theoretical Computer Science . , 2002.
10	MILLER, D. Higher-order quantification and proof search In: AMAST 2002 LNCS. , 2002. v.2422. p.60 - 74
11	MILLER, D., PIMENTEL, E. G. Using linear logic to reason about sequent systems In: Tableaux 2002 LNCS. , 2002.
12	MILLER, D. Encoding generic judgments: Preliminary results In: Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001) Electronic Notes of TCS. , 2001.
13	MILLER, D. Abstract Syntax for Variable Binders: An Overview In: Computational Logic - CL2000 LNAI. , 2000. v.1861.
14	MILLER, D., MCDOWELL, R. A Logic for Reasoning with Higher-Order Abstract Syntax In: Symposium on Logics in Computer Science . , 1997.
15	MILLER, D., PALAMIDESSI, C., MCDOWELL, R. Encoding Transition Systems in Sequent Calculus: Preliminary Report In: Linear Logic Workshop . , 1996.
16	MILLER, D. Logical Foundations for Open System Design In: Computing Surveys . , 1996.
17	MILLER, D. A Multiple-Conclusion Meta-Logic In: 1994 Symposium on Logics in Computer Science . , 1994.
18	MILLER, D. The p-calculus as a theory in linear logic: Preliminary results In: 1992 Workshop on Extensions to Logic Programming . , 1992.
19	MILLER, D., HODAS, J. Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract In: Logics in Computer Science . , 1991.
20	MILLER, D. Unification of Simply Typed Lambda-Terms as Logic Programming In: 1991 International Conference on Logic programming . , 1991.
21	MILLER, D., FELTY, A. Encoding a Dependent-Type l-Calculus in a Logic Programming Language In: 1990 Conference on Automated Deduction . , 1990.
22	MILLER, D., PARESCHI, R. Extending Definite Clause Grammars with Scoping Constructs In: 1990 International Conference in Logic Programming . , 1990.
23	MILLER, D., HANNAN, J. From Operational Semantics to Abstract Machines: Preliminary Results In: 1990 LISP and Functional Programming Conference . , 1990.
24	MILLER, D., HODAS, J. Representing Objects in a Logic Programming Language with Scoping Constructs In: 1990 International Conference in Logic Programming . , 1990.
25	MILLER, D. A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification In: Extentions of Logic Programming . , 1989.
26	MILLER, D. Lexical Scoping as Universal Quantification In: Sixth International Logic Programming Conference . , 1989.
27	MILLER, D., NADATHUR, G. An overview of lProlog In: Fifth Symposium on Logic Programming . , 1988.
28	MILLER, D., FELTY, A. Specifying theorem provers in a higher-order logic programming language In: 9th International Conference on Automated Deduction . , 1988.
29	MILLER, D., HANNAN, J. Uses of higher-order unification for implementing program transformers In: Fifth Symposium on Logic Programming . , 1988.
30	MILLER, D., NADATHUR, G. A logic programming approach to manipulating formulas and programs In: IEEE Symposium on Logic Programming . , 1987.
31	MILLER, D., NADATHUR, G., SCEDROV, A. Hereditary Harrop formulas and uniform proofs systems In: Second Anual Symposium on Logic in Computer Science . , 1987.
32	MILLER, D. A theory of modules for logic programming In: IEEE Symposium on Logic Programming . , 1986.
33	MILLER, D., FELTY, A. An integration of resolution and natural deduction theorem proving In: National Conference on Artificial Intelligence . , 1986.
34	MILLER, D., NADATHUR, G. Higher-order logic programming In: Third International Logic Programming Conference . , 1986.
35	MILLER, D., NADATHUR, G. Some uses of higher-order logic in computational linguistics In: 24th Annual Meeting of the Association for Computational Linguistics . , 1986.
36	MILLER, D. Expansion tree proofs and their conversion to natural deduction proofs In: 7th Conference on Automated Deduction . , 1984.
37	MILLER, D., ANDREWS, P. B., COHEN, E. L. A look at TPS In: 6th Conference on Automated Deduction . , 1982.

1	Jeremie Wajs. Design and implementation of a theorem prover for operational semantics. 2000. Dissertação (Computer Science) - The Pennsylvania State University
2	Alexander Betis. Object Programming, Linear Logic and Java. 1999. Dissertação (Computer Science) - The Pennsylvania State University
3	Joshua Hodas. Object-Oriented Programming in Logic Programming. 1990. Dissertação (Computer Science) - University of Pennsylvania
4	Amy Felty. Using extended tactics to do proof transformations. 1986. Dissertação (Computer Science) - University of Pennsylvania
5	Greg Hager. Computational aspects of proofs in modal logic. 1985. Dissertação (Computer Science) - University of Pennsylvania

1	Alwen Tiu. A Logical Framework for Reasoning about Logical Specifications. 2004. Tese (Theoretical Computer Science) - Ecole Polytechnique - Paris
2	Jeremie Wajs. Reasoning about logic programs using definitions and induction. 2002. Tese (Computer Science) - The Pennsylvania State University
3	Elaine Gouvêa Pimentel. Linear Logic and the specification of sequent systems. 2001. Tese (Ciência da Computação) - Universidade Federal de Minas Gerais
4	Raymond McDowell. Ray McDowell. 1997. Tese (Computer Science) - The Pennsylvania State University
5	Chuck Liang. Object-language substitution and unification in meta-logic. 1995. Tese (Computer Science) - University of Pennsylvania
6	Jawahar Chirimar. Proof Theoretic Approach To Specification Languages. 1995. Tese (Computer Science) - University of Pennsylvania
7	Joshua Hodas. Logic Programming in Intuitionistic Linear Logic: Theory, Design, and Implementation. 1993. Tese (Computer Science) - University of Pennsylvania
8	John Hannan. Proof-theoretic methods for analysis of functional programs. 1990. Tese (Computer Science) - University of Pennsylvania
9	Amy Felty. Implementing theorem provers in a higher-order logic programming language. 1989. Tese (Computer Science) - University of Pennsylvania
10	Gopalan Nadathur. A higher-order logic as the basis for logic programming. 1986. Tese (Computer Science) - University of Pennsylvania

Informações complementares
Orientações em andamento	3
Produção bibliográfica
Artigos publicados em periódicos	15
Completos	15
Trabalhos publicados em anais de eventos	37
Completos	37
Livros ou capítulos de livros	9
Livros publicados	1
Capítulos de livros publicados	8
Orientação concluída
Dissertações de mestrado	5
Teses de doutorado	10