Dale Miller
Possui graduação em B S Mathematics pela Lebanon Valley College(1978), doutorado em Mathematics pela Carnegie Mellon University(1983), pós-doutorado pela University of Edinburgh(1991), pós-doutorado pela University of Glasgow(1991), pós-doutorado pela Universitá degli Studi di Pisa(1994), pós-doutorado pela Universita Degli Studi Genova(1996), pós-doutorado pela Università di Siena(1997) e pós-doutorado pela Universite d'Aix-Marseille III (Droit, Econ. et Sciences)(2002). Atualmente é Directeur de Recherche da Institut National de Recherche En Informatique Et En Automatique e professor titular da École Polytechnique. Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Computação.
Informações coletadas do Lattes em 22/11/2022
Acadêmico
Formação acadêmica
Doutorado em Mathematics
1978 - 1983
Carnegie Mellon University
Título: L-calculus
Orientador: Peter Andrews
Grande área: Ciências Exatas e da Terra / Área: Matemática / Subárea: Álgebra / Especialidade: Lógica Matemática. Setores de atividade: Outros.
Pós-doutorado
2002 - 2002
Pós-Doutorado. , Universite d'Aix-Marseille III (Droit, Econ. et Sciences). , Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.
1997 - 1997
Pós-Doutorado. , Università di Siena. , Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.
1996 - 1996
Pós-Doutorado. , Universita Degli Studi Genova. , Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.
1994 - 1994
Pós-Doutorado. , Universitá degli Studi di Pisa. , Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.
1991 - 1991
Pós-Doutorado. , University of Glasgow. , Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.
1990 - 1991
Pós-Doutorado. , University of Edinburgh. , Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.
Idiomas
Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Italiano
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Francês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Áreas de atuação
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Lógicas e Semântica de Programas.
Grande área: Ciências Exatas e da Terra / Área: Matemática / Subárea: Álgebra/Especialidade: Lógica Matemática.
Orientou
PARSIFAL; Início: 2009; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris; (Orientador);
PARSIFAL; Início: 2009; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris; (Orientador);
PARSIFAL; Início: 2009; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris; (Orientador);
PARSIFAL; Início: 2009; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris; (Orientador);
PARSIFAL; Início: 2009; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris; (Orientador);
Design and implementation of a theorem prover for operational semantics; 2000; 0 f; Dissertação (Mestrado em Computer Science) - The Pennsylvania State University,; Orientador: Dale Miller;
Object Programming, Linear Logic and Java; 1999; 0 f; Dissertação (Mestrado em Computer Science) - The Pennsylvania State University,; Orientador: Dale Miller;
Object-Oriented Programming in Logic Programming; 1990; 0 f; Dissertação (Mestrado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Using extended tactics to do proof transformations; 1986; 0 f; Dissertação (Mestrado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Computational aspects of proofs in modal logic; 1985; 0 f; Dissertação (Mestrado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique; 2008; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris,; Orientador: Dale Miller;
A linear approach to the proof-theory of least and greatest fixed points; 2008; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris,; Orientador: Dale Miller;
A Logical Framework for Reasoning about Logical Specifications; 2004; Tese (Doutorado em Theoretical Computer Science) - Ecole Polytechnique - Paris,; Orientador: Dale Miller;
Reasoning about logic programs using definitions and induction; 2002; 0 f; Tese (Doutorado em Computer Science) - The Pennsylvania State University,; Orientador: Dale Miller;
Linear Logic and the specification of sequent systems; 2001; 0 f; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Minas Gerais,; Orientador: Dale Miller;
Ray McDowell; 1997; 0 f; Tese (Doutorado em Computer Science) - The Pennsylvania State University,; Orientador: Dale Miller;
Proof Theoretic Approach To Specification Languages; 1995; 0 f; Tese (Doutorado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Object-language substitution and unification in meta-logic; 1995; 0 f; Tese (Doutorado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Logic Programming in Intuitionistic Linear Logic: Theory, Design, and Implementation; 1993; 0 f; Tese (Doutorado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Proof-theoretic methods for analysis of functional programs; 1990; 0 f; Tese (Doutorado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Implementing theorem provers in a higher-order logic programming language; 1989; 0 f; Tese (Doutorado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
A higher-order logic as the basis for logic programming; 1986; 0 f; Tese (Doutorado em Computer Science) - University of Pennsylvania,; Orientador: Dale Miller;
Produções bibliográficas
-
MILLER, D. . Logic and Logic Programming: a personal account. Newsletter of the Association for Logic Programming, v. 16, n.1, 2006.
-
MILLER, D. ; TIU, A. . A Proof Theory for Generic Judgments. ACM Transactions on Computational Logic , v. 6, n.4, p. 749-783, 2005.
-
MILLER, D. ; PALAMIDESSI, C. ; MCDOWELL, R. . Encoding Transition Systems in Sequent Calculus. Theoretical Computer Science , v. 294, n.3, p. 411-437, 2003.
-
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.
-
MILLER, D. ; MCDOWELL, R. . Cut-Elimination for a Logic with Definitions and Induction. Theoretical Computer Science , v. 232, p. 91-119, 2000.
-
MILLER, D. ; PALAMIDESSI, C. . Foundational Aspects of Syntax. ACM Computing Surveys , v. 31, n.3, 1999.
-
MILLER, D. . Forum: A multiple-conclusion specification logic. Theoretical Computer Science , v. 165, n.1, p. 201-232, 1996.
-
MILLER, D. ; HODAS, J. . Logic programming in a fragment of intuitionistic linear logic. Information And Computation, v. 110, n.2, p. 327-365, 1994.
-
MILLER, D. ; HANNAN, J. . From operational semantics to abstract machines. Mathematical Structures In Computer Science, v. 2, n.4, p. 415-459, 1992.
-
MILLER, D. . Unification under a mixed prefix. Journal of Symbolic Computation , v. 14, p. 321-358, 1992.
-
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.
-
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.
-
MILLER, D. ; NADATHUR, G. . Higher-order Horn clauses. Journal of the Association for Computing Machinery , v. 37, n.4, p. 777-814, 1990.
-
MILLER, D. . A logical analysis of modules in logic programming. Journal of Logic Programming , v. 6, p. 79-108, 1989.
-
MILLER, D. . A compact representation of proofs. Studia Logica, v. 46, n.4, p. 345-368, 1987.
-
MILLER, D. ; NADATHUR, G. . lProlog: An Introduction to the Language and its Logic. , 2003.
-
MILLER, D. . Overview of linear logic programming. In: Thomas Ehrhard; Jean-Yves Girard; Paul Ruet; Phil Scott. (Org.). Linear Logic in Computer Science. : Cambridge University Press, 2004, v. 316, p. 119-150.
-
MILLER, D. ; PIMENTEL, E. G. . Linear logic as a framework for specifying sequent calculus. In: Jan Van Eijck; Vincent Van Oostrom; Albert Visser. (Org.). Lecture Notes in Logic. Illinois: Association for symbolic logic, 2004, v. 17, p. 111-135.
-
MILLER, D. ; NADATHUR, G. . Higher-order Logic Programming. In: Dov M. Gabbay; C. J. Hogger; J. A. Robinson. (Org.). Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford: Clarendon Press, 1998, v. , p. 499-590.
-
MILLER, D. . Sequent Calculus and the Specification of Computation. In: U. Berger; H. Schwichtenberg. (Org.). Computational Logic. : Springer, 1997, v. , p. -.
-
MILLER, D. . Logic Programming and Meta-Logic. In: H. Schwichtenberg. (Org.). The Logic of Computation. : Springer-Verlag, 1997, v. , p. 265-308.
-
MILLER, D. . Abstractions in logic programming. In: Pieirgiorgio Odifreddi. (Org.). Logic and Computer Science. : Academic Press, 1990, v. , p. 329-359.
-
MILLER, D. ; HANNAN, J. . A Meta-Language for Functional Programming. In: H. Abramson; M. Rogers. (Org.). Meta-Programming in Logic Programming. : MIT Press, 1989, v. , p. 453-476.
-
MILLER, D. ; ANDREWS, P. B. ; COHEN, E. L. ; PFENNING, F. . Automating higher order logic. In: W. W. Bledsoe; D. W. Loveland. (Org.). Automated Theorem Proving: After 25 Years. : AMS, 1984, v. , p. 169-192.
-
CHAUDHURI, K. ; MILLER, D. ; SAURIN, A. . Canonical Sequent Proofs via Multi-Focusing. In: Fifth IFIP International Conference on Theoretical Computer Science (TCS2008, Track B),, 2008, Boston. IFIP International Federation for Information Processing, 2008. v. 273. p. 383-396.
-
NIGAM, V. ; MILLER, D. . Focusing in linear meta-logic. In: International Joint Conference on Automated Reasoning (IJCAR 2008), 2008. LNCS, 2008. v. 5195. p. 507-522.
-
DELANDE, O. ; MILLER, D. . A neutral approach to proof and refutation in MALL. In: LICS 2008, 2008, Pittsburgh. Proceedings of LICS 2008, 2008.
-
GACEK, A. ; MILLER, D. ; NADATHUR, G. . Combining generic judgments with recursive definitions. In: LICS 2008, 2008, Pittsburgh. Proceedings of LICS 2008, 2008.
-
MILLER, D. . An overview of a proof theoretical approach to reasoning about computation. In: LFMTP08, 2008. Proceedings of LFMTP08, 2008.
-
GACEK, A. ; MILLER, D. ; NADATHUR, G. . Reasoning in Abella about Structural Operational Semantics Specifications. In: LFMTP08, 2008. Proceedings of LFMTP08, 2008.
-
MILLER, D. . Formalizing SOS specifications in logic. In: SOS08, 2008. Proceedings of SOS08, 2008.
-
BAELDE, D. ; MILLER, D. . Least and greatest fixed points in linear logic. In: LPAR 2007, 2007, Yerevan. Proceedings of LSFA 2007, 2007.
-
LIANG, C. ; MILLER, D. . Focusing and Polarization in Intuitionistic Logic. In: CSL'07: Computer Science Logic, 2007. LNCS, 2007. v. 4646. p. 451-465.
-
MILLER, D. ; NIGAM, V. . Incorporating tables into proofs. In: CSL'07: Computer Science Logic, 2007. LNCS, 2007. v. 4646. p. 466-480.
-
MILLER, D. ; SAURIN, A. . From proofs to focused proofs: a modular proof of focalization in Linear Logic. In: CSL'07: Computer Science Logic, 2007. LNCS, 2007. v. 4646. p. 405-419.
-
BAELDE, D. ; GACEK, A. ; MILLER, D. ; NADATHUR, G. ; TIU, A. . The Bedwyr system for model checking over syntactic expressions. In: CADE 2007: 21th Conference on Automated Deduction, 2007. LNAI, 2007. v. 4603. p. 391-397.
-
MILLER, D. . Representing and reasoning with operational semantics. In: IJCAR'06, 2006, Seattle. Proceedings of IJCAR'06, 2006.
-
MILLER, D. . Collection analysis for Horn clause programs: Extended Abstract. In: PPDP'06 (Eighth ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming), 2006, Veneza. Proceedings of PPDP'06, 2006.
-
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, 2005.
-
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, 2005.
-
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, 2005.
-
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, 2005. v. 3835. p. 352-366.
-
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.
-
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, 2004. v. 184. p. 79-101.
-
MILLER, D. ; TIU, A. . A Proof Theory for Generic Judgments: An extended abstract. In: LICS, 2003, Ottawa. Proceedings IEEE Computer Society 2003, 2003. p. 118-127.
-
MILLER, D. . Encryption as an abstract data-type: An extended abstract. In: Foundations of Computer Security, 2003, Stanford. Electronic Notes in Theoretical Computer Science, 2003. v. 84. p. 1-12.
-
MILLER, D. ; TIU, A. . Encoding Generic Judgments. In: 22nd Foundations of Software Technology and Theoretical Computer Science, 2002.
-
MILLER, D. . Higher-order quantification and proof search. In: AMAST 2002, 2002. LNCS. v. 2422. p. 60-74.
-
MILLER, D. ; PIMENTEL, E. G. . Using linear logic to reason about sequent systems. In: Tableaux 2002, 2002. LNCS.
-
MILLER, D. . Encoding generic judgments: Preliminary results. In: Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001), 2001. Electronic Notes of TCS.
-
MILLER, D. . Abstract Syntax for Variable Binders: An Overview. In: Computational Logic - CL2000, 2000. LNAI. v. 1861.
-
MILLER, D. ; MCDOWELL, R. . A Logic for Reasoning with Higher-Order Abstract Syntax. In: Symposium on Logics in Computer Science, 1997.
-
MILLER, D. ; PALAMIDESSI, C. ; MCDOWELL, R. . Encoding Transition Systems in Sequent Calculus: Preliminary Report. In: Linear Logic Workshop, 1996.
-
MILLER, D. . Logical Foundations for Open System Design. In: Computing Surveys, 1996.
-
MILLER, D. . A Multiple-Conclusion Meta-Logic. In: 1994 Symposium on Logics in Computer Science, 1994.
-
MILLER, D. . The p-calculus as a theory in linear logic: Preliminary results. In: 1992 Workshop on Extensions to Logic Programming, 1992.
-
MILLER, D. ; HODAS, J. . Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract. In: Logics in Computer Science, 1991.
-
MILLER, D. . Unification of Simply Typed Lambda-Terms as Logic Programming. In: 1991 International Conference on Logic programming, 1991.
-
MILLER, D. ; PARESCHI, R. . Extending Definite Clause Grammars with Scoping Constructs. In: 1990 International Conference in Logic Programming, 1990.
-
MILLER, D. ; HODAS, J. . Representing Objects in a Logic Programming Language with Scoping Constructs. In: 1990 International Conference in Logic Programming, 1990.
-
MILLER, D. ; HANNAN, J. . From Operational Semantics to Abstract Machines: Preliminary Results. In: 1990 LISP and Functional Programming Conference, 1990.
-
MILLER, D. ; FELTY, A. . Encoding a Dependent-Type l-Calculus in a Logic Programming Language. In: 1990 Conference on Automated Deduction, 1990.
-
MILLER, D. . A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. In: Extentions of Logic Programming, 1989.
-
MILLER, D. . Lexical Scoping as Universal Quantification. In: Sixth International Logic Programming Conference, 1989.
-
MILLER, D. ; HANNAN, J. . Uses of higher-order unification for implementing program transformers. In: Fifth Symposium on Logic Programming, 1988.
-
MILLER, D. ; NADATHUR, G. . An overview of lProlog. In: Fifth Symposium on Logic Programming, 1988.
-
MILLER, D. ; FELTY, A. . Specifying theorem provers in a higher-order logic programming language. In: 9th International Conference on Automated Deduction, 1988.
-
MILLER, D. ; NADATHUR, G. . A logic programming approach to manipulating formulas and programs. In: IEEE Symposium on Logic Programming, 1987.
-
MILLER, D. ; NADATHUR, G. ; SCEDROV, A. . Hereditary Harrop formulas and uniform proofs systems. In: Second Anual Symposium on Logic in Computer Science, 1987.
-
MILLER, D. . A theory of modules for logic programming. In: IEEE Symposium on Logic Programming, 1986.
-
MILLER, D. ; FELTY, A. . An integration of resolution and natural deduction theorem proving. In: National Conference on Artificial Intelligence, 1986.
-
MILLER, D. ; NADATHUR, G. . Higher-order logic programming. In: Third International Logic Programming Conference, 1986.
-
MILLER, D. ; NADATHUR, G. . Some uses of higher-order logic in computational linguistics. In: 24th Annual Meeting of the Association for Computational Linguistics, 1986.
-
MILLER, D. . Expansion tree proofs and their conversion to natural deduction proofs. In: 7th Conference on Automated Deduction, 1984.
-
MILLER, D. ; ANDREWS, P. B. ; COHEN, E. L. . A look at TPS. In: 6th Conference on Automated Deduction, 1982.
-
MILLER, D. . A Proof-Theoretic Approach to the Static Analysis of Logic Programs. Studies in Logic , 2009.
-
MILLER, D. ; LIANG, C. . Focusing and Polarization in Linear, Intuitionistic, and Classical Logic. Theoretical Computer Science , 2009.
Histórico profissional
Endereço profissional
-
École Polytechnique, Laboratoire D'informatique. , PALAISEAU Cedex, 91128 - Paris, - França, Telefone: (33) 169333803, URL da Homepage:
Experiência profissional
2002 - Atual
Institut National de Recherche en Informatique et en AutomatiqueVínculo: Outro, Enquadramento Funcional: Directeur de Recherche, Carga horária: 0, Regime: Dedicação exclusiva.
Atividades
-
Direção e administração, Futurs, .,Cargo ou função, Directeur de Recherche.
-
Pesquisa e desenvolvimento , Futurs, .,Linhas de pesquisa
2002 - Atual
Ecole PolytechniqueVínculo: Outro, Enquadramento Funcional: Professor titular, Carga horária: 20
Atividades
-
Pesquisa e desenvolvimento , Lix, .,Linhas de pesquisa
-
Ensino, Computer Science, Nível: Pós-Graduação,Disciplinas ministradas, Logic and Computer Science
1997 - 2002
The Pennsylvania State UniversityVínculo: Outro, Enquadramento Funcional: Professor titular, Carga horária: 40, Regime: Dedicação exclusiva.
Atividades
-
Pesquisa e desenvolvimento , Computer Science Department, .,Linhas de pesquisa
-
Ensino, Computer Science, Nível: Pós-Graduação,Disciplinas ministradas, Semantics of Programming Languages, Type theory, Logic and Computer Science
-
Direção e administração, Computer Science Department, Cse.,Cargo ou função, Head.
1983 - 1997
University of PennsylvaniaVínculo: Outro, Enquadramento Funcional: Professor titular, Carga horária: 40, Regime: Dedicação exclusiva.
Atividades
-
Pesquisa e desenvolvimento , Department Of Computer Science, .,Linhas de pesquisa
-
Ensino, Computer Science, Nível: Pós-Graduação,Disciplinas ministradas, Semantics of Programming Languages, Logic and Computer Science, Type theory
1978 - 1983
Carnegie Mellon UniversityVínculo: Outro, Enquadramento Funcional: Research Assistant, Carga horária: 40, Regime: Dedicação exclusiva.
Atividades
-
Pesquisa e desenvolvimento , Department Of Mathematics, .,Linhas de pesquisa
1977 - 1978
NIST Boulder LaboratoriesVínculo: Outro, Enquadramento Funcional: Mathematician, Carga horária: 40, Regime: Dedicação exclusiva.
Atividades
-
Pesquisa e desenvolvimento , Ai Lab, .,Linhas de pesquisa
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todos os processos de Dale Miller e sempre que o nome aparecer em publicações dos Diários Oficiais, avisaremos por e-mail e pelo painel do usuário
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todas as movimentações desse processo e sempre que o processo aparecer em publicações dos Diários Oficiais e nos Tribunais, avisaremos por e-mail e pelo painel do usuário
Confirma a exclusão?