BibSLEIGH — Dale

Travelled to:

1 × Australia
1 × Estonia
1 × Germany
1 × Israel
1 × Portugal
1 × Switzerland
1 × The Netherlands
13 × USA
2 × Canada
2 × Poland
2 × Spain
3 × Italy
3 × United Kingdom
4 × France

Collaborated with:

∅ G.Nadathur C.Liang V.Nigam A.P.Felty J.Hannan J.S.Hodas I.Gazeau C.Palamidessi D.Baelde A.Gacek O.Delande A.Saurin A.F.Tiu R.McDowell R.Pareschi A.Scedrov E.L.Gunter Z.Chihani F.Renaud K.Chaudhuri S.Hetzl Z.Snow E.L.Cohen P.B.Andrews F.Pfenning A.Tiu C.Neuwirth R.Chandhok D.Kaufer P.Erion J.H.Morris G.T.Leavens J.Abrial D.S.Batory M.J.Butler A.Coglio K.Fisler E.C.R.Hehner C.B.Jones S.L.P.Jones M.Sitaraman D.R.Smith A.Stump

Talks about:

logic (24) program (18) proof (12) order (6) abstract (5) higher (5) focus (5) languag (4) linear (4) intuitionist (3)

Person: Dale Miller

DBLP: Miller:Dale

Facilitated 3 volumes:

Contributed to:

2015

2013

2012

2010

2009

2008

2007

2006

2004

2003

2000

1997

1994

1992

1991

1990

1988

1987

1986

1984

1982

Wrote 46 papers:

PPDP-2015-Miller #logic programming #proving: Proof checking and logic programming (DM), p. 18.
CADE-2013-ChihaniMR #first-order #logic #proving: Foundational Proof Certificates in First-Order Logic (ZC, DM, FR), pp. 162–177.
LICS-2013-LiangM #logic: Unifying Classical and Intuitionistic Logics for Computational Control (CL, DM), pp. 283–292.
QAPL-2013-GazeauMP #difference #privacy #semantics: Preserving differential privacy under finite-precision semantics (IG, DM, CP), pp. 1–18.
CSL-2012-ChaudhuriHM #approach #calculus: A Systematic Approach to Canonicity in the Classical Sequent Calculus (KC, SH, DM), pp. 183–197.
QAPL-2012-GazeauMP #analysis #float #robust #source code: A non-local method for robustness analysis of floating point programs (IG, DM, CP), pp. 63–76.
IJCAR-2010-BaeldeMS #induction #proving #theorem proving: Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.
LICS-2009-LiangM #calculus #proving: A Unified Sequent Calculus for Focused Proofs (CL, DM), pp. 355–364.
PPDP-2009-NigamM #algorithm #linear #logic #specification: Algorithmic specifications in linear logic with subexponentials (VN, DM), pp. 129–140.
IJCAR-2008-NigamM #linear #logic: Focusing in Linear Meta-logic (VN, DM), pp. 507–522.
LICS-2008-DelandeM #approach #proving: A Neutral Approach to Proof and Refutation in MALL (OD, DM), pp. 498–508.
LICS-2008-GacekMN #recursion: Combining Generic Judgments with Recursive Definitions (AG, DM, GN), pp. 33–44.
CADE-2007-BaeldeGMNT #model checking: The Bedwyr System for Model Checking over Syntactic Expressions (DB, AG, DM, GN, AT), pp. 391–397.
CSL-2007-LiangM #logic: Focusing and Polarization in Intuitionistic Logic (CL, DM), pp. 451–465.
CSL-2007-MillerN #proving: Incorporating Tables into Proofs (DM, VN), pp. 466–480.
CSL-2007-MillerS #composition #linear #logic #proving: From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic (DM, AS), pp. 405–419.
GPCE-2006-LeavensABBCFHJMJSSS #roadmap #verification: Roadmap for enhanced languages and methods to aid verification (GTL, JRA, DSB, MJB, AC, KF, ECRH, CBJ, DM, SLPJ, MS, DRS, AS), pp. 221–236.
IJCAR-2006-Miller #reasoning #representation #semantics: Representing and Reasoning with Operational Semantics (DM), pp. 4–20.
PPDP-2006-Miller #analysis #horn clause #source code: Collection analysis for Horn clause programs (DM), pp. 179–188.
CSL-2004-Miller #quantifier: Bindings, Mobility of Bindings, and the “generic judgments”-Quantifier: An Abstract (DM), p. 24.
LICS-2003-MillerT #proving: A Proof Theory for Generic Judgments: An extended abstract (DM, AFT), pp. 118–127.
CL-2000-Miller #overview #perspective #syntax: Abstract Syntax for Variable Binders: An Overview (DM), pp. 239–253.
LICS-1997-McDowellM #higher-order #logic #reasoning #syntax: A Logic for Reasoning with Higher-Order Abstract Syntax (RM, DM), pp. 434–445.
ALP-1994-Miller #logic programming #multi #source code #specification #using: Specifications Using Multiple-Conclusion Logic Programs (DM), pp. 3–4.
LICS-1994-Miller #logic #multi: A Multiple-Conclusion Meta-Logic (DM), pp. 272–281.
PLILP-1994-Miller #logic programming #multi #source code #specification #using: Specifications Using Multiple-Conclusion Logic Programs (DM), pp. 3–4.
CSCW-1992-NeuwirthCKEMM #collaboration #flexibility: Flexible Diff-ing in a Collaborative Writing System (CN, RC, DK, PE, JHM, DM), pp. 147–154.
ICLP-1991-Miller #logic programming #unification: Unification of Simply Typed Lamda-Terms as Logic Programming (DM), pp. 255–269.
ICLP-1991-Miller91a #logic #logic programming #tutorial: Logics for Logic Programming: A Tutorial (DM), p. 911.
LICS-1991-HodasM #linear #logic programming: Logic Programming in a Fragment of Intuitionistic Linear Logic (JSH, DM), pp. 32–42.
CADE-1990-FeltyGMP #prolog #tutorial #λ-calculus: Tutorial on Lambda-Prolog (APF, ELG, DM, FP), p. 682.
CADE-1990-FeltyM #encoding #logic programming #programming language #λ-calculus: Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language (APF, DM), pp. 221–235.
CLP-1990-HodasM90 #logic programming #representation: Representing Objects in a Logic Programming Langueage with Scoping Constructs (JSH, DM), pp. 511–526.
CLP-1990-Miller90 #higher-order #logic programming: Higher-Order Logic Programming (DM), p. 784.
CLP-1990-PareschiM90 #definite clause grammar: Extending Definite Clause Grammars with Scoping Constructs (RP, DM), pp. 373–389.
LFP-1990-HannanM #automaton #semantics: From Operational Semantics to Abstract Machines: Preliminary Results (JH, DM), pp. 323–332.
CADE-1988-FeltyGHMNS #logic programming #named #programming language #prolog #λ-calculus: Lambda-Prolog: An Extended Logic Programming Language (APF, ELG, JH, DM, GN, AS), pp. 754–755.
CADE-1988-FeltyM #higher-order #logic programming #programming language #proving #specification #theorem proving: Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.
JICSCP-1988-HannanM88 #higher-order #implementation #unification: Uses of Higher-Order Unification for Implementing Program Transformers (JH, DM), pp. 942–959.
JICSCP-1988-NadathurM88 #overview #prolog: An Overview of λ-PROLOG (GN, DM), pp. 810–827.
LICS-1987-MillerNS #proving: Hereditary Harrop Formulas and Uniform Proof Systems (DM, GN, AS), pp. 98–105.
SLP-1987-MillerN87 #approach #logic programming #source code: A Logic Programming Approach to Manipulating Formulas and Programs (DM, GN), pp. 379–388.
ICLP-1986-MillerN86 #higher-order #logic programming: Higher-Order Logic Programming (DM, GN), pp. 448–462.
SLP-1986-Miller86 #formal method #logic programming: A Theory of Modules for Logic Programming (DM), pp. 106–114.
CADE-1984-Miller #deduction #proving: Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs (DM), pp. 375–393.
CADE-1982-MillerCA: A Look at TPS (DM, ELC, PBA), pp. 50–69.