16 citations · 62 across the 19 of their papers we have counts for
20 papers
A system of inference based on proof search: an extended abstract
Dale Miller
Gentzen designed his natural deduction proof system to ``come as close as possible to actual reasoning.'' Indeed, natural deduction proofs closely resemble the static structure of…
A Survey of the Proof-Theoretic Foundations of Logic Programming
Dale Miller
Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory…
Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Dale Miller, Ivan Scagnetto
This volume contains a selection of papers presented at LFMTP 2019, the 14th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on J…
Functional programming with lambda-tree syntax
Ulysse Gérard, Dale Miller, Gabriel Scherer
We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this appro…
A Proof Theory for Model Checking: An Extended Abstract
Quentin Heath, Dale Miller
While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide…
Well-Typed Languages are Sound
Matteo Cimini, Dale Miller, Jeremy G. Siek
Type soundness is an important property of modern programming languages. In this paper we explore the idea that "well-typed languages are sound": the idea that the appropriate typi…