Daniel R. Licata

Submitted to POPL ’09 Dependently Typed Programming with Domain-Specific Logics (2009)

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...

Submitted to PLPV ’09 Positively Dependent Types (2009)

We define a dependent programming language in which programmers can define and compute with domain-specific logics, such as an access-control logic that statically prevents unauthorized access to...

Submitted to POPL ’09 Dependently Typed Programming with Domain-Specific Logics (2009)

This paper is part of a line of work on using the logical techniques of polarity and focusing to design a dependent programming language, with particular emphasis on programming with deductive...

Under consideration for publication in J. Functional Programming 1 Mechanizing Metatheory in a Logical Framework (2009)

We define a dependent programming language in which programmers can define and compute with domain-specific logics, such as an access-control logic that statically prevents unauthorized access to...

Focusing on Computation with Binding (2008)

The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the...

Mechanizing a Decision Procedure for Coproduct Equality (2008)

Abstract—Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both...

Arbob Ahmad, Daniel R. Licata, Robert Harper

In many applications of λ-calculi, it is essential to compare λ-terms for equality. For example, type checking a dependently typed programming language requires deciding equality of its terms and...

Under consideration for publication in J. Functional Programming 1 Mechanizing Metatheory in a Logical Framework (2008)

Under consideration for publication in J. Functional Programming 1 Mechanizing Metatheory in a Logical Framework (2008)

The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the...

Focusing on Binding and Computation (2008)

The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the...

Focusing on Binding and Computation (2008)

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...

Dependently typed programming with domain-specific logics (thesis proposal). Available from http://www.cs.cmu.edu/~drl (2008)

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...

Daniel R. Licata

We propose a thesis defending the following statement: The logical notions of polarity and focusing provide a foundation for dependently typed programming with domain-specific logics, with...

Focusing on binding and computation (2008)

Mechanizing Language Definitions (2006)

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...

The cult of the bound variable: The 9 th annual ICFP programming contest (2006)

We present a technical introduction to mechanizing language definitions and meta-theory using LF and Twelf. LF is a logical framework designed for representing languages that are specified by...

Tom Murphy, Vii Daniel, Spoonhower Chris Casinghino, Daniel R. Licata, Karl Crary, Robert Harper

The annual ICFP Programming Contest has become one of the premiere programming competitions in the world. The 9 th incarnation of the contest, “The Cult of the Bound Variable, ” was held in July...

A Formulation of Dependent ML with Explicit Equality Proofs (2005)

A Formulation of Dependent ML with Explicit Equality Proofs (2005)

We study a calculus that supports dependent programming in the style of Xi and Pfenning's Dependent ML. Xi and Pfenning's language determines equality of static data using a built-in...

A formulation of Dependent ML with explicit equality proofs (2005)

We study a calculus that supports dependent programming in the style of Xi and Pfenning's Dependent ML. Xi and Pfenning's language determines equality of static data using a built-in...