Dale Miller
Dale Miller

Homepage at LIX

  Affiliation history
· University of Pennsylvania
· Carnegie Mellon University
· Pennsylvania State University
· Ecole Polytechnique
· INRIA Futurs
· University of Thessaly
· Laboratoire d'Informatique de l'Ecole Polytechnique
Bibliometrics: publication history
Publication years1982-2015
Publication count81
Citation Count926
Available for download17
Downloads (6 Weeks)29
Downloads (12 Months)220
Downloads (cumulative)6,161
Average downloads per article362.41
Average citations per article11.43
Professional ACM Member
Arrow RightAuthor only
· Editor only
· Advisor only
· Other only
· All roles

See all colleagues of this author

See all subject areas

See all author supplied keywords

Project background Author-Izer logoAuthor-Izer Service


Use the QR code to
Scan, Save, Share
 this Author Page

81 results found Export Results: bibtex | endnote | acmref | csv

Result 1 – 20 of 81
Result page: 1 2 3 4 5

Sort by:

1 published by ACM
Proof checking and logic programming
July 2015 PPDP '15: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming
Publisher: ACM
Citation Count: 0
Downloads (6 Weeks): 1,   Downloads (12 Months): 15,   Downloads (Overall): 15

Full text available: PDFPDF
In a world where trusting software systems is problematic, formal methods and formal proofs should be able to help. Proof checking can play an important role in establishing trust since such checkers can be smaller and easier to verify than, for example, entire theorem provers or model checkers. Proof checking ...
Keywords: focused proof systems, proof checking, foundational proof certificates

2 published by ACM
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
Kaustuv Chaudhuri, Matteo Cimini, Dale Miller
January 2015 CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs
Publisher: ACM
Citation Count: 0
Downloads (6 Weeks): 2,   Downloads (12 Months): 25,   Downloads (Overall): 25

Full text available: PDFPDF
Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to ...
Keywords: process calculus, abella, λ-tree syntax, bisimulation-up-to, co-induction

3 published by ACM
Foundational proof certificates: making proof universal and permanent
September 2013 LFMTP '13: Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice
Publisher: ACM
Citation Count: 0
Downloads (6 Weeks): 1,   Downloads (12 Months): 5,   Downloads (Overall): 17

Full text available: PDFPDF
Consider a world where exporting proof evidence into a declarative, universal, and permanent format is taken as ``feature zero'' for computational logic systems. In such a world, provers will be able to communicate and share theorems and proofs; libraries can archive and organize proofs; and marketplaces of proofs would be ...
Keywords: proof certificates, focused proof systems

A formal framework for specifying sequent calculus proof systems
Dale Miller, Elaine Pimentel
January 2013 Theoretical Computer Science: Volume 474, February, 2013
Publisher: Elsevier Science Publishers Ltd.
Citation Count: 1

Intuitionistic logic and intuitionistic type systems are commonly used as frameworks for the specification of natural deduction proof systems. In this paper we show how to use classical linear logic as a logical framework to specify sequent calculus proof systems and to establish some simple consequences of the specified sequent ...
Keywords: Linear logic, Cut elimination, Logical frameworks, Sequent calculus, Proof systems

A Two-Level Logic Approach to Reasoning About Computations
Andrew Gacek, Dale Miller, Gopalan Nadathur
July 2012 Journal of Automated Reasoning: Volume 49 Issue 2, August 2012
Publisher: Springer-Verlag New York, Inc.
Citation Count: 9

Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding ...
Keywords: ∇-quantification, Two-level logic, λ-tree syntax, Generic judgments, Nominal abstraction

Programming with Higher-Order Logic
Dale Miller, Gopalan Nadathur
June 2012
Citation Count: 11

Formal systems that describe computations over syntactic structures occur frequently in computer science. Logic programming provides a natural framework for encoding and animating such systems. However, these systems often embody variable binding, a notion that must be treated carefully at a computational level. This book aims to show that a ...

A proposal for broad spectrum proof certificates
December 2011 CPP'11: Proceedings of the First international conference on Certified Programs and Proofs
Publisher: Springer-Verlag
Citation Count: 4

Recent developments in the theory of focused proof systems provide flexible means for structuring proofs within the sequent calculus. This structuring is organized around the construction of “macro” level inference rules based on the “micro” inference rules which introduce single logical connectives. After presenting focused proof systems for first-order classical ...

Nominal abstraction
Andrew Gacek, Dale Miller, Gopalan Nadathur
December 2010 Information and Computation: Volume 209 Issue 1, January, 2011
Publisher: Academic Press, Inc.
Citation Count: 8

Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics ...
Keywords: λ-Tree syntax, Proof search, Reasoning about operational semantics, Generic judgments, Higher-order abstract syntax

Reasoning about computations using two-levels of logic
November 2010 APLAS'10: Proceedings of the 8th Asian conference on Programming languages and systems
Publisher: Springer-Verlag
Citation Count: 0

We describe an approach to using one logic to reason about specifications written in a second logic. One level of logic, called the "reasoning logic", is used to state theorems about computational specifications. This logic is classical or intuitionistic and should contain strong proof principles such as induction and co-induction. ...

A Framework for Proof Systems
Vivek Nigam, Dale Miller
July 2010 Journal of Automated Reasoning: Volume 45 Issue 2, August 2010
Publisher: Springer-Verlag New York, Inc.
Citation Count: 6

Linear logic can be used as a meta-logic to specify a range of object-level proof systems. In particular, we show that by providing different polarizations within a focused proof system for linear logic, one can account for natural deduction (normal and non-normal), sequent proofs (with and without cut), and tableaux ...
Keywords: Meta-logic, Linear logic, Logical framework, Focusing

Focused inductive theorem proving
David Baelde, Dale Miller, Zachary Snow
July 2010 IJCAR'10: Proceedings of the 5th international conference on Automated Reasoning
Publisher: Springer-Verlag
Citation Count: 9

Focused proof systems provide means for reducing and structuring the non-determinism involved in searching for sequent calculus proofs. We present a focused proof system for a first-order logic with inductive and co-inductive definitions in which the introduction rules are partitioned into an asynchronous phase and a synchronous phase. These focused ...

Finding unity in computational logic
April 2010 ACM-BCS '10: Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference
Publisher: British Computer Society
Citation Count: 1
Downloads (6 Weeks): 4,   Downloads (12 Months): 13,   Downloads (Overall): 88

Full text available: PDFPDF
While logic was once developed to serve philosophers and mathematicians, it is increasingly serving the varied needs of computer scientists. In fact, recent decades have witnessed the creation of the new discipline of Computational Logic. While Computation Logic can claim involvement in diverse areas of computing, little has been done ...
Keywords: proof theory, unity of logic, computational logic, sequent calculus, focused proof systems

13 published by ACM
Proof search specifications of bisimulation and modal logics for the π-calculus
Alwen Tiu, Dale Miller
January 2010 ACM Transactions on Computational Logic (TOCL): Volume 11 Issue 2, January 2010
Publisher: ACM
Citation Count: 5
Downloads (6 Weeks): 4,   Downloads (12 Months): 20,   Downloads (Overall): 239

Full text available: PDFPDF
We specify the operational semantics and bisimulation relations for the finite π-calculus within a logic that contains the ∇ quantifier for encoding generic judgments and definitions for encoding fixed points. Since we restrict to the finite case, the ability of the logic to unfold fixed points allows this logic to ...
Keywords: bisimulation, modal logics, ∇ quantifier, generic judgments, Proof search, higher-order abstract syntax, λ-tree syntax, π-calculus

Focusing and polarization in linear, intuitionistic, and classical logics
Chuck Liang, Dale Miller
October 2009 Theoretical Computer Science: Volume 410 Issue 46, November, 2009
Publisher: Elsevier Science Publishers Ltd.
Citation Count: 26

A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various ...
Keywords: Classical logic, Focused proof system, Sequent calculus, Intuitionistic logic

15 published by ACM
Algorithmic specifications in linear logic with subexponentials
Vivek Nigam, Dale Miller
September 2009 PPDP '09: Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming
Publisher: ACM
Citation Count: 12
Downloads (6 Weeks): 0,   Downloads (12 Months): 12,   Downloads (Overall): 93

Full text available: PDFPDF
The linear logic exponentials !,? are not canonical: one can add to linear logic other such operators, say ! l ,? 1 , which may or may not allow contraction and weakening, and where l is from some pre-ordered set of labels. We shall call these additional operators subexponentials and ...
Keywords: proof search, linear logic, subexponentials

A Unified Sequent Calculus for Focused Proofs
Chuck Liang, Dale Miller
August 2009 LICS '09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science
Publisher: IEEE Computer Society
Citation Count: 4

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical logic, intuitionistic logic, and multiplicative-additive linear logic are derived as fragments of LKU by increasing the sensitivity of specialized structural rules to polarity information. We develop a unified, streamlined ...
Keywords: Proof theory, focused proof systems, linear logic

Formalizing Operational Semantic Specifications in Logic
July 2009 Electronic Notes in Theoretical Computer Science (ENTCS): Volume 246, August, 2009
Publisher: Elsevier Science Publishers B. V.
Citation Count: 1

We review links between three logic formalisms and three approaches to specifying operational semantics. In particular, we show that specifications written with (small-step and big-step) SOS, abstract machines, and multiset rewriting, are closely related to Horn clauses, binary clauses, and (a subset of) linear logic, respectively. We shall illustrate how ...
Keywords: big-step SOS semantics, Operational semantics, multiset rewriting, small-step SOS semantics, specifications

Reasoning in Abella about Structural Operational Semantics Specifications
Andrew Gacek, Dale Miller, Gopalan Nadathur
December 2008 Electronic Notes in Theoretical Computer Science (ENTCS): Volume 228, January, 2009
Publisher: Elsevier Science Publishers B. V.
Citation Count: 7

The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses @l-tree syntax to treat object language binding and encodes binding related properties in generic judgments. Further, object language specifications are embedded directly into the reasoning framework through recursive definitions. The ...
Keywords: λ-tree syntax, Abella, object language binding, Structural operational semantics

Focusing in Linear Meta-logic
Vivek Nigam, Dale Miller
August 2008 IJCAR '08: Proceedings of the 4th international joint conference on Automated Reasoning
Publisher: Springer-Verlag
Citation Count: 2

It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a variety of sequent calculus proof systems. Here, we show that if we adopt different focusingannotations for such linear logic ...

A Neutral Approach to Proof and Refutation in MALL
Olivier Delande, Dale Miller
June 2008 LICS '08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science
Publisher: IEEE Computer Society
Citation Count: 4

We propose a setting in which the search for a proof of B or a refutation of B (a proof of not B) can be carried out simultaneously. In contrast with the usual approach in automated deduction, we do not need to first commit to either proving B or to ...
Keywords: neutral approach, linear logic, game semantics

The ACM Digital Library is published by the Association for Computing Machinery. Copyright © 2016 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us