Frank Pfenning

Church and Curry: Combining Intrinsic and Extrinsic Typing (2009)

Abstract. In this paper we describe Imogen, a theorem prover for intuitionistic propositional logic using the focused inverse method. We represent fine-grained control of the search behavior by...

Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic (2009)

Church’s formulation of the simple theory of types [1] has the pleasing property that every well-formed term has a unique type. The type is thus an intrinsic attribute of a term. Furthermore, we...

Linear Logical Approximations ∗ (2009)

Abstract. In this paper we describe Imogen, a theorem prover for intuitionistic propositional logic using the focused inverse method. We represent fine-grained control of the search behavior by...

Robert J. Simmons, Frank Pfenning

The abstract interpretation of programs relates the exact semantics of a programming language to an approximate semantics that can be effectively computed. We show that, by specifying operational...

General Terms (2009)

Robert J. Simmons, Frank Pfenning

The abstract interpretation of programs relates the exact semantics of a programming language to an approximate semantics that can be effectively computed. We show that, by specifying operational...

Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic (2009)

Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Language]: Mathematical Logic--Lambda calculus and related systems (2009)

Abstract. In this paper we describe Imogen, a theorem prover for intuitionistic propositional logic using the focused inverse method. We represent fine-grained control of the search behavior by...

General Terms Languages, Theory (2009)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Abstract Ordered type theory is an extension of linear type theory in whichvariables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of...

A bidirectional refinement type system for LF (2009)

William Lovas, Frank Pfenning

We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are...

Linear Logical Algorithms (2009)

Robert J. Simmons, Frank Pfenning

Abstract. Bottom-up logic programming can be used to declaratively specify many algorithms in a succinct and natural way, and McAllester and Ganzinger have shown that it is possible to define a cost...

Linear Logic (2009)

Higher-order pattern complement and the strict λ-calculus (2009)

This material is in rough draft form and is likely to contain errors. Furthermore, citations are in no way adequate or complete. Please do not cite or distribute this document. This work was...

General Terms Languages, Theory (2009)

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Abstract Ordered type theory is an extension of linear type theory in whichvariables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of...

Programming Languages for Embedded Systems (2009)

Sebastian Thrun, Frank Pfenning, Sungwoo Park, Jonathan Moody

Problem: Sensor-based embedded systems have to cope with uncertainty. Uncertainty arises from sensorlimitations, environment dynamics, and lack of knowledge at the design time of embedded system....

Contextual Modal Type Theory ALEKSANDAR NANEVSKI Harvard University and (2009)

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this paper we investigate the consequences of relativizing these concepts to explicitly...

Contents (2008)

Some Imp ortant Issues in Language Design (2008)

Fall 1999, revised Spring 2004. This includes revised excerpts from the

T Yp, Hongw Ei Xi, Frank Pfenning

erro rdetection ffl Co rrect and efficient implementation ffl La rge scale programming ffl Program verification ffl Program do cumentation 2 Advantages of Typ e Systems ffl Capturing program erro rs...

A Bidirectional Refinement Type System for LF Abstract (2008)

William Lovas, Frank Pfenning

We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are...

ktefinement ‘1’ypes tor ML (2008)

Tim Freeman, Frank Pfenning

T$’e describe a refinement of ML’s type system allow-ing the specification of recursively defined subtypes of user-defined datatypes. The resulting system of rejirze-meni f,ypes preserves...

Carnegie Mellon UniversityE-mail: { (2008)

Abstract. We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as...

An Authorization Logic with Explicit Time ∗ (2008)

Abstract We present a constructive authorization logic where themeanings of connectives are defined by their associated inference rules. This ensures that the logical reading of ac-cess control...

Contextual Modal Type Theory ALEKSANDAR NANEVSKI Harvard University and (2008)

We present an authorization logic that permits reasoning with explicit time. Following a proof-theoretic approach, we study the meta-theory of the logic, including cut elimination. We also...

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this paper we investigate the consequences of relativizing these concepts to explicitly...

Abstract Dependent Types in Practical Programming* (Extended Abstract) (2008)

Abstract. We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as...

TPS: A Theorem Proving Systemfor Classical Type Theory (2008)

hongweiQcse.ogi.edu We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the...

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi

AbstractThis is a description of T PS, a theorem proving system for classical type theory (Church's typedl-calculus). T PS has been designed to be a general research tool for manipulating wffs...

F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—lambda calculus and (2008)

Contextual Modal Type Theory ALEKSANDAR NANEVSKI Harvard University and (2008)

Abstract. We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of typed �-calculi...

Abstract Eliminating Array Bound Checking Through Dependent Types* (2008)

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this paper we investigate the consequences of relativizing these concepts to explicitly...

Intuitionistic Letcc via Labelled Deduction Abstract (2008)

We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the...

Jason Reed, Frank Pfenning

The well-known embedding of intuitionistic logic into classical modal logic means that intuitionistic logic can be viewed as a calculus of labelled deduction on multiple-conclusion sequents, where...

A Monadic Analysis of Information Flow Security with Mutable State (2008)

Karl Crary Aleksey, Frank Pfenning

July 13, 2004 We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysisis based on a logic of information flow derived from lax logic and the...

Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)

Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...

Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...

General Terms: Languages,Theory (2008)

Higher-order pattern complement and the strict λ-calculus (2008)

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of typed λ-calculi and...

Reasoning About Deductions in Linear Logic (Invited Talk) (2008)

We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be...

Contextual Modal Type Theory ALEKSANDAR NANEVSKI Harvard University and (2008)

Linear logic has been described as a logic of state. Many complex systems involving state transitions, such as imperative programming languages, concurrent systems, protocols, planning problems,...

Memory management General Terms (2008)

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this paper we investigate the consequences of relativizing these concepts to explicitly...

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

Abstract Elf: A Language for Logic Definition (2008)

Verified Metaprogramming, Frank Pfenning

We describe Elf, a metalanguage for proof manipulation environments that are independent of any particular logical system. Elf is intended for meta-programs such as theorem provers, proof...

MFPS XV Preliminary Version Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic (2008)

Memory management General Terms (2008)

We present a sequent calculus for intuitionistic non-commutative linear logic (IN-CLL), show that it satisfies cut elimination, and investigate its relationship to a natural deduction system for the...

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

On a Logical Foundation for Explicit Substitutions (2008)

Abstract Higher-Order Abstract Syntax ∗ (2008)

Traditionally, calculi of explicit substitution [1] have been conceived as an implementation technique for β-reduction and studied with the tools of rewriting theory. This computational view has...

Frank Pfenning, Conal Elliott

We describe motivation, design, use, and implementation of higher-order abstract syntax as a central representation for programs, formulas, rules, and other syntactic objects in program manipulation...

Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)

Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...

Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...

A Schema for Adding Dependent Types to ML ∗ (2008)

LOGICAL FRAMEWORKS—A BRIEF INTRODUCTION (2008)

We present an approach to enriching the type system of ML with a form of dependent types, where index objects are restricted to constraint domains C, leading to the DML(C) language schema. Pure...

Languages, Experimentation (2008)

Abstract. A logical framework is a meta-language for the formalization of deductive systems. We provide a brief introduction to logical frameworks and their methodology,

Sungwoo Park, Frank Pfenning

As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages that treat probability distributions as primitive datatypes. Most...

Resource Management for the Inverse Method in Linear Logic ⋆ (2008)

HOOTS99 Preliminary Version On proving syntactic properties of CPS programs (2008)

Abstract. One central aspect of proof search in linear logic is resource management. Strategies for efficient resource management have been developed for backward-directed calculi, such as top-down...

Higher-order program transformations raise new challenges for proving properties of their output, since they resist traditional, first-order proof techniques. In this work, we consider (1) the...

Automated Theorem Proving in a Simple Meta Logic for LF (2008)

Abstract. We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as...

Abstract. Higher-order representation techniques allow elegant encodings of logics and programming languages in the logical framework LF, but unfortunately they are fundamentally incompatible with...

Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Language]: Mathematical Logic--Lambda calculus and related systems (2008)

Abstract. We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as...

Under consideration for publication in J. Functional Programming 1 Meta-Programming with Names and Necessity (2008)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

1 Introduction Properties of Terms in Continuation-Passing Style in an Ordered Logical Framework (2008)

Meta-programming is a discipline of writing programs in a certain programming language that generate, manipulate or execute programs written in another language. In a typed setting, meta-programming...

General (2008)

Pablo López, Frank Pfenning, Jeff Polakow, Kevin Watkins

Lolli is a logic programming language based on the asynchronous propositions of intuitionistic linear logic. It uses a backward chaining, backtracking operational semantics. In this paper we extend...

Gilles Dowek, Claude Kirchner, Thérèse Hardin, Frank Pfenning

Abstract (2008)

Following the general method and related completeness results on using explicit substitutions to perform higher-order unification proposed in [5], we investigate in this paper the case of...

Higher-order pattern complement and the strict λ-calculus (2008)

Under consideration for publication in J. Functional Programming 1 Meta-Programming with Names and Necessity (2008)

Meta-programming is a discipline of writing programs in a certain programming language that generate, manipulate or execute programs written in another language. In a typed setting, meta-programming...

and (2008)

Higher-order pattern complement and the strict λ-calculus (2008)

Received; revised; accepted We present the linear type theory λ Π−◦& ⊤ as the formal basis for LLF, a conservative extension of the logical framework LF. LLF combines the expressive power...

Abstract A Monadic Analysis of Information Flow Security with Mutable State (2008)

We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be...

General Terms: Languages, Design (2008)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Philip Wickline, Peter Lee, Frank Pfenning, Rowan Davies

A well-known technique for improving the performance of computer programs is to separate the computations into distinct stages so that the results of early computations can be profitably exploited by...

Under consideration for publication in J. Functional Programming 1 Staged Computation with Names and Necessity (2008)

Carnegie Mellon UniversityE-mail: { (2008)

Staging is a programming technique for dividing the computation in order to exploit the early availability of some arguments. In the early stages the program uses the available arguments to generate,...

Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)

Abstract We present a constructive authorization logic where themeanings of connectives are defined by their associated inference rules. This ensures that the logical reading of ac-cess control...

Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...

Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...

Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)

Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...

Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...

ETPS: A System to Help Students Write Formal Proofs (2008)

Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi

ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...

Abstract Invited Talk (2008)

Intersection Types Revisited, Frank Pfenning

Church’s system of simple types has proven to be remarkably robust: call-by-name, call-by-need, and call-by-value languages, with or without effects, and even logical frameworks can be based on the...

Under consideration for publication in J. Functional Programming 1 Staged Computation with Names and Necessity (2008)

Contextual Modal Type Theory ALEKSANDAR NANEVSKI Harvard University and (2008)

Staging is a programming technique for dividing the computation in order to exploit the early availability of some arguments. In the early stages the program uses the available arguments to generate,...

Under consideration for publication in J. Functional Programming 1 A Monadic Analysis of Information Flow Security with Mutable State (2008)

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this paper we investigate the consequences of relativizing these concepts to explicitly...

Karl Crary, Frank Pfenning

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

A Bidirectional Refinement Type System for LF Abstract (2008)

William Lovas, Frank Pfenning

We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are...

Under consideration for publication in J. Functional Programming 1 A Monadic Analysis of Information Flow Security with Mutable State (2008)

Karl Crary Aleksey, Karl Crary, Frank Pfenning

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Deepak Garg And, Deepak Garg, Frank Pfenning

We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as computation. The...

An Authorization Logic with Explicit Time 1 (2008)

An Authorization Logic with Explicit Time 1 (2008)

We present an authorization logic that permits reasoning with explicit time. Following a prooftheoretic approach, we study the meta-theory of the logic, including cut elimination. We also demonstrate...

Lecture Notes on Intermediate Representation 15-411: Compiler Design (2008)

We present an authorization logic that permits reasoning with explicit time. Following a prooftheoretic approach, we study the meta-theory of the logic, including cut elimination. We also demonstrate...

Lecture Notes on Liveness Analysis 15-411: Compiler Design (2008)

In this lecture we discuss the “middle end ” of the compiler. After the source has been parsed we obtain an abstract syntax tree, on which we carry out various static analyses to see if the...

Modal Types for Mobile Code (2008)

We will see different kinds of program analyses in the course, most of them for the purpose of program optimization. The first one, liveness analysis, is required for register allocation. A variable...

Tom Murphy Vii, Frank Pfenning, Peter Sewell

In this dissertation I argue that modal type systems provide an elegant and practical means for controlling local resources in spatially distributed computer programs. A distributed program is one...

Imogen User’s Manual (2008)

Lecture Notes on Dataflow Analysis 15-411: Compiler Design (2008)

Imogen is a theorem prover for propositional intuitionistic logic. For download and installation instructions, consult the Imogen website [?]. 2

A Logic for Reasoning About Time-Dependent Access Control Policies (2008)

In this lecture we first extend liveness analysis to handle memory references and then consider neededness analysis which is similar to liveness and used to discover dead code. Both liveness and...

Henry Deyoung, Frank Pfenning, Deepak Garg

are those of the author and should not be interpreted as representing official policies, either expressed or implied, of any sponsoring institution, the U.S. government, or any other entity....

On the Overhead of CPS (2007)

The Formal Specification of Programming Languages (2007)

Continuation-passing style (CPS) is often criticized to be more expensive than the usual direct style of functional programming. By structure, CPS functions indeed are passed one extra argument (the...

Myra Vaninwegen, Elsa Gunter, T Bell Laboratories, Frank Pfenning

In this thesis proposal we propose to prove type preservation for Core SML. Type preservation is stated roughly as follows: if a phrase has type and evaluates to a value v, then v has type. In...

Chapter 1 Logical frameworks (2007)

Frank Pfenning, Don Sannella, Jan Smith

2 Abstract syntax......................................... 5 2.1 Uni-typed representations................................ 6

Chapter 1 Logical frameworks (2007)

Frank Pfenning, Don Sannella, Jan Smith

Unification in a (2007)

Calculus With Intersection, Michael Kohlhase, Frank Pfenning

We propose related algorithms for unification and constraint simplification in !& , a refinement of the simply-typed -calculus with subtypes and bounded intersection types. !& is intended as...

Unification in a lambda-Calculus with Intersection Types (2007)

Michael Kohlhase, Frank Pfenning

We propose related algorithms for unification and constraint simplification in !& , a refinement of the simply-typed -calculus with subtypes and bounded intersection types. !& is intended as...

Efficient Resource Management (2007)

Submitted To, Iliano Cervesato, Joshua S. Hodas, Frank Pfenning

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and...

Proc. Workshop on Strategies in Automated Deduction (2007)

Bernhard Gramlich, Frank Pfenning

. The Maude system incorporates reflective capabilities that enable quite sophisticated strategies to be expressed very conveniently. Maude's strategy languages have been used to control the...

Seminar on Linear Logic and Application - Suggested Topics (2007)

Frank Pfenning, G. Plotkin, Logical Frameworks

xth Annual Symposium on Logic in Computer Science, Amsterdam, July 15-18, 1991. [LS94a] P. Lincoln and A. Scedrov. First order linear logic without modalities is NEXPTIMEhard. Theoretical Computer...

Efficient Resource Management (2007)

Submitted To, Iliano Cervesato, Joshua S. Hodas, Frank Pfenning

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and...

1 (2007)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Abstract. We present the propositional fragment CLF0 of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations...

Type Assignment for Intersections and Unions in Call-by-Value Languages (2007)

Joshua Dun Eld, Frank Pfenning

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional...

Chapter 4 The Inverse Method (2007)

Anatoli Degtyarev, Andrei Voronkov, Gregory Mints, Frank Pfenning, Renate Schmidt

1.1 Backward and forward reasoning.......................... 181

ETPS: A System to Help Students Write Formal Proofs (2007)

Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi

ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in rst-order logic or higher-order logic. It enables students to concentrate on the...

1 (2007)

Carsten Schurmann, Frank Pfenning

Abstract. Coverage checking is the problem of deciding whether any closed term of a given type is an instance of at least one of a given set of patterns. It can be used to verify if a function...

Under consideration for publication in J. Functional Programming 1 Meta-Programming with Names and Necessity (2007)

Resource Management for the Inverse Method in Linear Logic (2007)

Meta-programming is a discipline of writing programs in a certain programming language that generate, manipulate or execute programs written in another language. In a typed setting, meta-programming...

On proving syntactic properties of (2007)

Abstract. One central aspect of proof search in linear logic is resource management. Strategies for efficient resource management have been developed for backward-directed calculi, such as top-down...

Belmina Dzafic, Olivier Danvy, Olivier Danvy, Belmina Dza C, Frank Pfenning, Frank Pfenning

et al.: On proving syntactic properties of CPS programs BRICS Basic Research in Computer Science

Higher-order pattern complement and the strict λ-calculus (2007)

On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) (2007)

We address the problem of complementing higher-order patterns without repetitions of existential variables. Dierently from the rst-order case, the complement of a pattern cannot, in general, be...

Towards a Functional Library for Fault-Tolerant Grid Computing (2007)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...

Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...

Towards a Functional Library for Fault-Tolerant Grid Computing (2007)

Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...

Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...

2 (2007)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Abstract. We present the propositional fragment CLF0 of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations...

which includes intuitionistic functions (!), linear functions (\Gammaffi), additive pairing (&), and additive unit (2007)

Higher-order pattern complement and the strict λ-calculus (2007)

We present the spine calculus S!\Gammaffi&? as an efficient representation for the linear-calculus

Uni cation in a -Calculus with Intersection Types (2007)

We address the problem of complementing higher-order patterns without repetitions of existential variables. Dierently from the rst-order case, the complement of a pattern cannot, in general, be...

z (2007)

Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component parts, but rather the...

Michael Kohlhase, Frank Pfenning

We propose related algorithms for unication and constraint simplication in , a renement of the simply-typed -calculus with subtypes and bounded intersection types. is intended as the basis of a...

Contents (2007)

Andreas Abel, Acknowledgements Ralph Matthes, Frank Pfenning, Brigitte Pientka

Notes for a course given at Carnegie Mellon University during the Spring semester of 2001. Please send comments to fp@cs.cmu.edu. These notes are to be published by Cambridge University Press....

!E (2007)

Parigot's -Calculus Proof terms for the implicational fragment of classical logic in natural deduction style Raw terms: M:: = x j x:M j MM j a:N (Unnamed) terms N:: = [a]M Named terms Typing...

Contents (2007)

Alberto Momigliano, Le Hr, Frank Pfenning

We address the problem of complementing higher-order patterns without repetitions of free variables. Dierently from the rst-order case, the complement of a pattern cannot, in general, be described by...

for Linear Logic Proof Search (2007)

Abstract. The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses...

Linear Logic (2007)

Human-Readable Machine-Veriable Proofs for Teaching Constructive Logic (2007)

This material is in rough draft form and is likely to contain errors. Furthermore, citations are in no way adequate or complete. Please do not cite or distribute this document. This work was...

A Concurrent Logical Framework: the (2007)

Abstract. A linear syntax for natural deduction proofs in rst-order intuitionistic logic is presented, which has been an eective tool for teaching logic. The proof checking algorithm is also given,...

Propositional Fragment Kevin, Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

We present the propositional fragment CLF0 of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations in an...

A Symmetric Modal Lambda Calculus for Distributed Computing # (2007)

Tom Murphy Vii, Karl Crary, Robert Harper, Frank Pfenning

We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...

A Symmetric Modal Lambda Calculus for Distributed Computing # (2007)

Tom Murphy Vii, Karl Crary, Robert Harper, Frank Pfenning

We present a foundational language for spatially distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal...

2 (2007)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Abstract. We present CLF, a dependently typed logical framework for concurrent computations with several novel features, including the use of synchronous linear connectives inside a monad. We...

Type Assignment for Intersections and Unions (2007)

Joshua Dun Eld, Frank Pfenning

We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional language. The...

Type Refinements (2007)

Modal Types for Mobile Code (draft) (2007)

Despite many concentrated research efforts in various areas such as software engineering, programming languages, and logic, software today is not fundamentally more reliable than it was a decade ago....

Tom Murphy Vii, Frank Pfenning, Peter Sewell

compilers, types In this dissertation I argue that modal type systems provide an elegant and practical means for controlling local resources in spatially distributed computer programs. A distributed...

Avoiding Spurious Causal Dependencies via Proof Irrelevance in a Concurrent Logical Framework (2007)

Ruy Ley-wild, Frank Pfenning

The Concurrent Logic Framework (CLF) is a foundational type theory for encoding concurrent computations by representing resources with linearity and encapsulating the effects of concurrency in a...

Project Summary Manifest Security (2007)

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure...

Project Summary Manifest Security (2007)

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure...

Project Summary Manifest Security (2007)

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure...

An authorization logic with explicit time (2007)

An authorization logic with explicit time (2007)

We present an authorization logic that permits reasoning with explicit time. Following a proof-theoretic approach, we study the meta-theory of the logic, including cut elimination. We also...

15-819K: Logic Programming Lecture 18 Proof Terms (2006)

We present an authorization logic that permits reasoning with explicit time. Following a proof-theoretic approach, we study the meta-theory of the logic, including cut elimination. We also...

A linear logic of authorization and knowledge (2006)

In this lecture we will substantiate an earlier claim that logic programming not only permits the representation of specifications and the implementation of algorithm, but also the realization of...

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter

15-819K: Logic Programming Lecture 8 Completion (2006)

A linear logic of authorization and knowledge (2006)

In this lecture we extend the ground backtracking semantics to permit free variables. This requires a stronger normal form for programs. After introducing this normal form related to the so-call...

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter

Abstract. We propose a logic for specifying security policies at a very high level of abstraction. The logic accommodates the subjective nature of affirmations for authorization and knowledge without...

15-819K: Logic Programming Lecture 26 (2006)

Frank Pfenning, L. Datalog

In this lecture we describe Datalog, a decidable fragment of Horn logic. Briefly, Datalog disallows function symbols, which means that the so-called Herbrand universe of ground instances of...

15-819K: Logic Programming Lecture 7 Lifting (2006)

15-819K: Logic Programming Lecture 2 Data Structures (2006)

Lifting is the name for turning a search calculus with ground judgments into one employing free variables. Unification might be viewed as the result of lifting a ground equality judgment, but we...

Now the rule for simultaneous conjunction is (2006)

In this second lecture we introduce some simple data structures such as lists, and simple algorithms on them such as as quicksort or mergesort. We also introduce some first considerations of types...

15-819K: Logic Programming Lecture 3 Induction (2006)

In this lecture we address the resource management problem in linear logic programming. We also give some small but instructive examples of linear logic programming, supplementing the earlier peg...

15-819K: Logic Programming Lecture 21 Forward Chaining (2006)

One of the reasons we are interested in high-level programming languages is that, if properly designed, they allow rigorous reasoning about properties of programs. We can prove that our programs...

15-819K: Logic Programming Lecture 19 Verifying Progress (2006)

In this lecture we go from the view of logic programming as derived from inference rules for atomic propositions to one with explicit logical connectives. We have made this step before in order to...

15-819K: Logic Programming Lecture 6 Unification (2006)

In this lecture we discuss another logic program analysis, namely verifying the progress property. Progress guarantees that a predicate can never fail for arbitrary values of its input arguments....

15-819K: Logic Programming Lecture 20 Bottom-Up Logic Programming (2006)

In this lecture we take the essential step towards making the choice of goal and rule instantiation explicit in the operational semantics. This consists of describing an algorithm for a problem...

15-819K: Logic Programming Lecture 9 Types (2006)

In this lecture we return to the view that a logic program is defined by a collection of inference rules for atomic propositions. But we now base the operational semantics on reasoning forward from...

Manifest Security for Distributed Information (2006)

In this lecture we introduce types into logic programming, primarily to distinguish meaningful from meaningless terms and propositions, thereby capturing errors early during program development. 9.1...

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

What is the best way to build programs that compute with data sources controlled by multiple principals, while ensuring compliance with the security policies of the principals involved? The objective...

L14.2 Cut Elimination (2006)

Frank Pfenning, B Subderivation D

In this lecture we consider how to prove that connectives are asynchronous as goals and then consider cut elimination, one of the most important and fundamental properties of logical systems. We then...

15-819K: Logic Programming Lecture 23 Linear Monadic Logic Programming (2006)

15-819K: Logic Programming Lecture 24 (2006)

In this lecture we extend the observations about forward and backward chaining from Horn logic to a rich set of linear connectives. In order to control the interaction between forward and backward...

L11.2 Difference Lists (2006)

In this lecture we return to the treatment of logic variables. In Prolog and some extensions we have considered, logic variables are global, and equations involving logic variables are solved by...

L1.2 Logic Programming (2006)

In this lecture we look at programming techniques that are specific to logic programming, or at least significantly more easily expressed and reasoned about in logic programming than other paradigms....

15-819K: Logic Programming Lecture 4 Operational Semantics (2006)

In this first lecture we give a brief introduction to logic programming. We also discuss administrative details of the course, although these are not included here, but can be found on the course web...

15-819K: Logic Programming Lecture 5 Backtracking (2006)

In this lecture we begin in the quest to formally capture the operational semantics in order to prove properties of logic programs that depend on the way proof search proceeds. This will also allow...

15-819K: Logic Programming Lecture 10 (2006)

In this lecture we refine the operational semantics further to explicit represent backtracking. We prove this formulation to be sound. From earlier examples it should be clear that it can no longer...

Frank Pfenning, L. Polymorphism

In this lecture we extend the system of simple types from the previous lecture to encompass polymorphism. There are some technical pitfalls, and some plausible systems do not satisfy type...

15-819K: Logic Programming Lecture 22 (2006)

Frank Pfenning, L. Hyperresolution

In this lecture we lift the forward chaining calculus from the ground to the free variable case. The form of lifting required is quite different from the backward chaining calculus. For Horn logic,...

15-819K: Logic Programming Lecture 25 Substructural Operational Semantics (2006)

A linear logic of authorization and knowledge (2006)

In this lecture we combine ideas from the previous two lectures, linear monadic logic programming and higher-order abstract syntax, to present a specification technique for programming languages we...

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter

A Logical Characterization of Forward and Backward Chaining in the Inverse (2006)

Kaustuv Chaudhuri, Frank Pfenning, Greg Price

The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli's focusing strategy can be adapted for the inverse method in...

A Linear Logic of Authorization and Knowledge (2006)

Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, Michael Reiter

We propose a logic for specifying security policies at a very high level of abstraction. The logic accommodates the subjective nature of affirmations for authorization and knowledge without...

Non-Interference in Constructive Authorization Logic (2006)

Manifest Security for Distributed Information (2006)

We present a constructive authorization logic where the meanings of connectives are defined by their associated inference rules. This ensures that the logical reading of access control policies...

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

gical methods for specifying and verifying them. These properties will be formally verified against precise specifications written in a novel logic of authorization and information flow using...

Consumable Credentials in Logic-Based Access Control (2006)

Lujo Bauer, Lujo Bauer, Kevin D. Bowers, Kevin D. Bowers, Frank Pfenning, Frank Pfenning, ...

We present a framework to support consumable credentials in a logic-based distributed authorization system. Such credentials convey use-limited authority (e.g., to open a door once) or authority to...

Avoiding Causal Dependencies via Proof Irrelevance in a Concurrent Logical Framework (2006)

Ruy Ley-Wild, Frank Pfenning

The Concurrent Logic Framework (CLF) is a foundational type theory for encoding concurrent computations by representing resources with linearity and encapsulating the effects of concurrency in a...

A Logical Characterization of Forward and Backward (2006)

Chaining In The, Kaustuv Chaudhuri, Frank Pfenning, Greg Price

The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli's focusing strategy can be adapted for the inverse method in...

Manifest Security for Distributed Information (2006)

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

al methods for specifying and verifying them. These properties will be formally verified against precise specifications written in a novel logic of authorization and information flow using mechanized...

A linear logic of authorization and knowledge (2006)

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter

Abstract. We propose a logic for specifying security policies at a very high level of abstraction. The logic accommodates the subjective nature of affirmations for authorization and knowledge without...

A linear logic of authorization and knowledge (2006)

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter

Abstract. We propose a logic for specifying security policies at a very high level of abstraction. The logic accommodates the subjective nature of affirmations for authorization and knowledge without...

A linear logic of authorization and knowledge (2006)

Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, Michael Reiter

A logical characterization of forward and backward chaining in the inverse method (2006)

Kaustuv Chaudhuri, Frank Pfenning, Greg Price

Abstract. The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli’s focusing strategy can be adapted for the inverse...

Manifest Security for Distributed Information (2006)

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

What is the best way to build programs that compute with data sources controlled by multiple principals, while ensuring compliance with the security policies of the principals involved? The objective...

A logical characterization of forward and backward chaining in the inverse method (2006)

Kaustuv Chaudhuri, Frank Pfenning, Greg Price

A logical characterization of forward and backward chaining in the inverse method (2006)

Kaustuv Chaudhuri, Frank Pfenning, Greg Price, École Polytechnique

Abstract. The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli’s focusing strategy can be adapted for the inverse...

A linear logic of authorization and knowledge (2006)

Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, Michael Reiter

Abstract. We propose a logic for specifying security policies at a very high level of abstraction. The logic accommodates the subjective nature of affirmations for authorization and knowledge without...

Consumable credentials in logic-based access control (2006)

Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter

We present a method to implement consumable credentials in a logic-based distributed authorization system. Such credentials convey use-limited authority (e.g., to open a door once) or authority to...

Consumable credentials in logic-based access control (2006)

Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter

We present a method to implement consumable credentials in a logic-based distributed authorization system. Such credentials convey use-limited authority (e.g., to open a door once) or authority to...

Manifest Security for Distributed Information (2006)

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic

A linear logic of authorization and knowledge (2006)

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter

Abstract. We propose a logic for specifying security policies at a very high level of abstraction. The logic accommodates the subjective nature of affirmations for authorization and knowledge without...

15-819K: Logic Programming Lecture 13 Abstract Logic Programming (2006)

15-819K: Logic Programming Lecture 1 Logic Programming (2006)

In this lecture we discuss general criteria to judge whether a logic or a fragment of it can be considered a logic programming language. Taking such criteria as absolute is counterproductive, but...

Frank Pfenning, Frank Pfenning

In this first lecture we give a brief introduction to logic programming. We also discuss administrative details of the course, although these are not included here, but can be found on the course web...

L27.2 Constraint Logic Programming (2006)

[3] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992. (2006)

In this lecture we sketch constraint logic programming which generalizes the fixed structure of so-called uninterpreted function and predicate symbols of Horn logic. A common application is more...

Frank Pfenning, Jean-marc Andreoli, Remo Pareschi Lo, Behold Concurrent

This is the collection of all papers and reports cited in the lecture notes.

A probabilistic language based on sampling functions (2006)

Sungwoo Park, Frank Pfenning

As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages which treat probability distributions as primitive datatypes. Most...

15-819K: Logic Programming Lecture 12 Linear Logic (2006)

device at Carnegie Mellon University. (2005)

In this lecture we will rewrite the program for peg solitaire in a way that treats state logically, rather than as an explicit data structure. In order to allow this we need to generalize the logic...

Lujo Bauer, Frank Pfenning, Michael K. Reiter

We describe a project to advance security in distributed systems via the application of logical frameworks. At the heart of the effort lies an authorization logic which plays a triple role: (1) to...

Focusing the Inverse Method for Linear Logic (2005)

JFP 15 (2): 249--291, 2005. c (2005)

Focusing is traditionally seen as a means of reducing inessential nondeterminism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we construct a form...

A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (2005)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Staged Computation with Names and Necessity (2005)

We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. The central proof-theoretic insights underlying the prover...

Monadic Concurrent Linear Logic Programming (2005)

Staging is a programming technique for dividing the computation in order to exploit the early availability of some arguments. In the early stages the program uses the available arguments to generate,...

Pablo Lopez, Frank Pfenning, Jeff Polakow, Kevin Watkins

Lolli is a logic programming language based on the asynchronous propositions of intuitionistic linear logic. It uses a backward chaining, backtracking operational semantics. In this paper we extend...

Focusing the Inverse Method for Linear Logic (2005)

A Symmetric Modal Lambda Calculus for Distributed (2005)

Focusing is traditionally seen as a means of reducing inessential non-determinism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we construct a form...

Computing Tom Murphy, Tom Murphy, Vii Karl, Crary Robert Harper, Frank Pfenning

We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...

A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (2005)

Contextual Model Type Theory (2005)

We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. The central proof-theoretic insights underlying the prover...

Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka

this paper we investigate the consequences of relativizing these concepts to explicitly specified contexts. We obtain contextual modal logic and its type-theoretic analogue. Contextual modal type...

A Probabilistic Language based upon Sampling Functions (2005)

Sungwoo Park Frank, Frank Pfenning, Sebastian Thrun

probabilistic languages that treat probability distributions as primitive datatypes. Most probabilistic languages, however, focus only on discrete distributions and have limited expressive power. In...

A focusing inverse method theorem prover for first-order linear logic (2005)

Focusing the inverse method for linear logic (2005)

Abstract. We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. The central proof-theoretic insights underlying the...

Focusing the inverse method for linear logic (2005)

Abstract. Focusing is traditionally seen as a means of reducing inessential nondeterminism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we...

A probabilistic language based upon sampling functions (2005)

Abstract. Focusing is traditionally seen as a means of reducing inessential non-determinism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we...

A focusing inverse method theorem prover for first-order linear logic (2005)

As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages that treat probability distributions as primitive datatypes. Most...

A probabilistic language based upon sampling functions (2005)

Abstract. We present the theory and implementation of a theorem prover forfirst-order intuitionistic linear logic based on the inverse method. The central proof-theoretic insights underlying the...

A concurrent logical framework: The propositional fragment (2004)

As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages which treat probability distributions as primitive datatypes. Most...

Special member (2004)

Alwen F. Tiu, Padma Raghavan, Stephen Simpson, Frank Pfenning, Raj Acharya

*Signatures are on file in the Graduate School. We present a new logic, Linc, which is designed to be used as a framework for specifying and reasoning about operational semantics. Linc is an...

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Abstract. We present the propositional fragment CLF0 of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations...

A Symmetric Modal Lambda Calculus for Distributed Computing (2004)

Tom Murphy VII, Karl Crary, Robert Harper, Tom Murphy, Vii Karl, Crary Robert Harper, ...

We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...

Tridirectional Typechecking, Joshua Dunfield, Frank Pfenning

In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types.

Verifying Uniqueness in a Logical Framework (2004)

Penny Anderson, Frank Pfenning

We present an algorithm for verifying that some specified arguments of an inductively defined relation in a dependently typed #- calculus are uniquely determined by some other arguments. We prove it...

A Symmetric Modal Lambda Calculus for Distributed Computing (2004)

Tom Murphy VII, Karl Crary, Robert Harper, Tom Murphy, Vii Karl, Crary Robert Harper, ...

We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...

Tridirectional Typechecking, Joshua Dunfield Frank, Frank Pfenning

In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types....

A Symmetric Modal Lambda Calculus for Distributed Computing (2004)

Tom Murphy VII, Karl Crary, Robert Harper, Tom Murphy, Vii Karl, Crary Robert Harper, ...

We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...

Tridirectional Typechecking, Joshua Dunfield, Frank Pfenning

In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types....

A Probabilistic Language based upon Sampling Functions (2004)

A Symmetric Modal Lambda Calculus for Distributed (2004)

in solving various problems, researchers have designed probabilistic languages that treat probability distributions as primitive datatypes. Most probabilistic languages, however, focus only on...

Computing Tom Murphy, Tom Murphy, Vii Karl, Crary Robert Harper, Frank Pfenning

We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...

Specifying Properties of Concurrent Computations in CLF (2004)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

CLF (the Concurrent Logical Framework) is a language for specifying and reasoning about concurrent systems. Its most significant feature is the first-class representation of concurrent executions as...

A Probabilistic Language based upon Sampling Functions (2004)

Sungwoo Park Frank, Frank Pfenning

As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages that treat probability distributions as primitive datatypes. Most...

CLF: A Dependent Logical Framework for Concurrent Computations (2004)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

We present CLF, a dependently typed logical framework with several novel features supporting concurrent computations, in particular monads and synchronous linear connectives. We illustrate its...

Joshua Dunfield Frank, Frank Pfenning

In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types....

A symmetric modal lambda calculus for distributed computing (2004)

Tom Murphy, Vii Karl, Crary Robert Harper, Frank Pfenning

We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...

Specifying Properties of Concurrent Computations in CLF (2004)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

CLF (the Concurrent Logical Framework) is a language for specifying and reasoning about concurrent systems. Its most significant feature is the first-class representation of concurrent executions as...

A concurrent logical framework: The propositional fragment (2004)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Abstract. We present the propositional fragment CLF0 of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations...

Verifying uniqueness in a logical framework (2004)

Penny Anderson, Frank Pfenning

Abstract. We present an algorithm for verifying that some specified arguments of an inductively defined relation in a dependently typed λcalculus are uniquely determined by some other arguments. We...

Substructural operational semantics and linear destination-passing style (2004)

Verifying uniqueness in a logical framework (2004)

We introduce substructural operational semantics (SSOS), a presentation form for the semantics of programming languages. It combines ideas from structural operational semantics and type theories...

Penny Anderson, Frank Pfenning

Abstract. We present an algorithm for verifying that some specified arguments of an inductively defined relation in a dependently typed *- calculus are uniquely determined by some other arguments. We...

A symmetric modal lambda calculus for distributed computing (2004)

Tom Murphy, Vii Karl, Crary Robert Harper, Frank Pfenning

Abstract We present a foundational language for distributed programming, called Lambda 5, that addresses both mobilityof code and locality of resources. In order to construct our system, we appeal to...

A concurrent logical framework: The propositional fragment (2004)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Abstract. We present the propositional fragment CLF0 of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations...

Tridirectional Typechecking, Joshua Dunfield, Frank Pfenning

In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types....

A symmetric modal lambda calculus for distributed computing (2004)

Tom Murphy, Vii Karl, Crary Robert Harper, Frank Pfenning

Abstract We present a foundational language for distributed programming, called Lambda 5, that addresses both mobilityof code and locality of resources. In order to construct our system, we appeal to...

A learning algorithm for localizing people based on wireless signal strength that uses labeled and unlabeled data (2003)

2000. Material for this course is available at

Mary Berna, Brad Lisien, Brennan Sellner, Geoffrey Gordon, Frank Pfenning, Sebastian Thrun

We propose a probabilistic technique for localizing people through the signal strengths of a wireless IEEE 802.11b network. Our approach uses data labeled by ground truth position to learn a...

A type theory for memory allocation and data layout (2003)

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

Type assignment for intersections and unions in call-by-value languages (2003)

Type assignment for intersections and unions in call-by-value languages (2003)

A monadic analysis of information flow security with mutable state (2003)

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional...

A learning algorithm for localizing people based on wireless signal strength that uses labeled and unlabeled data (2003)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Mary Berna, Brennan Sellner, Brad Lisien, Sebastian Thrun, Geoffrey Gordon, Frank Pfenning

This paper summarizes a probabilistic approach for localizing people through the signal strengths of a wireless IEEE 802.11b network. Our approach uses data labeled by ground truth position to learn...

A type theory for memory allocation and data layout (2003)

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

A calculus for probabilistic languages (2003)

A type theory for memory allocation and data layout (2003)

Motivated by many practical applications that have to compute in the presence of uncertainty, we propose a monadic probabilistic language based upon the mathematical notion of sampling function. Our...

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

A type theory for memory allocation and data layout (2003)

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

Type assignment for intersections and unions in call-by-value languages (2003)

Abstract. We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such...

Type assignment for intersections and unions in call-by-value languages (2003)

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional...

Type assignment for intersections and unions in call-by-value languages (2003)

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional...

A type theory for memory allocation and data layout (2003)

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

Type assignment for intersections and unions in call-by-value languages (2003)

A Monadic Analysis of Information Flow Security with Mutable State (2003)

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional...

A Monadic Analysis of Information Flow Security with Mutable State (2003)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

A Modal Foundation for Meta-Variables (2003)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Aleksandar Nanevski, Ar Nanevski, Brigitte Pientka, Frank Pfenning

We report on work in progress regarding a foundation for the notion of meta-variable in logical frameworks and type theories. Our proposal is to treat meta-variables as modal variables in a modal...

A Coverage Checking Algorithm for LF (2003)

Optimizing Higher-Order Pattern Unification (2003)

Coverage checking is the problem of deciding whether any closed term of a given type is an instance of at least one of a given set of patterns. It can be used to verify if a function defined by...

Brigitte Pientka And, Brigitte Pientka, Frank Pfenning

We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such as...

A Concurrent Logical Framework II: Examples and Applications (2003)

Iliano Cervesato, Frank Pfenning, David Walker, Kevin Watkins

CLF is a new logical framework with an intrinsic notion of concurrency. It is designed as a conservative extension of the linear logical framework LLF with the synchronous connectives , 1, !, and 9...

ETPS: A System to Help Students Write Formal Proofs (2003)

Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi

ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...

A Type Theory for Memory Allocation and Data (2003)

Layout Extended Version, Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

A Linear Spine Calculus (2003)

Iliano Cervesato Advanced, Iliano Cervesato, Frank Pfenning

We present the spine calculus S as an efficient representation for the linear -calculus which includes unrestricted functions (!), linear functions ( ), additive pairing (&), and additive unit...

A Monadic Analysis of Information Flow Security with Mutable State (2003)

Karl Crary Aleksey, Karl Crary, Aleksey Kliger, Frank Pfenning

this paper, we will restrict our attention to secrecy properties. A variety of security-typed languages have been proposed, and several of them are both higher-order (i.e., support first-class...

A monadic analysis of information flow security with mutable state (2003)

A modal foundation for meta-variables (2003)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Ar Nanevski, Brigitte Pientka, Frank Pfenning

Abstract. We report on work in progress regarding a foundation for the notion of meta-variable in logical frameworks and type theories. Our proposal is to treat meta-variables as modal variables in a...

Type assignment for intersections and unions in call-by-value languages (2003)

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional...

Abstract. We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such...

A judgmental analysis of linear logic (2003)

Abstract. Coverage checking is the problem of deciding whether any closed term of a given type is an instance of at least one of a given set of patterns. It can be used to verify if a function...

A type theory for memory allocation and data layout (2003)

Abstract. We reexamine the foundations of linear logic, developing a system of natural deduction following Martin-Löf’s separation of judgments from propositions. Our construction yields a clean...

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

A Denotational Approach to Measuring Complexity in Functional Programs (2003)

Kathryn Van Stone, Frank Pfenning, Dana Scott, Carl Gunter

A monadic analysis of information flow security with mutable state (2003)

A learning algorithm for localizing people based on wireless signal strength that uses labeled and unlabeled data (2003)

Mary Berna, Brennan Sellner, Brad Lisien, Sebastian Thrun, Geoffrey Gordon, Frank Pfenning

This paper summarizes a probabilistic approach for localizing people through the signal strengths of a wireless IEEE 802.11b network. Our approach uses data labeled by ground truth position to learn...

A monadic analysis of information flow security with mutable state (2003)

Abstract. Coverage checking is the problem of deciding whether any closed term of a given type is an instance of at least one of a given set of patterns. It can be used to verify if a function...

A monadic analysis of information flow security with mutable state (2003)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Type assignment for intersections and unions in call-by-value languages (2003)

Abstract We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional...

A monadic analysis of information flow security with mutable state (2003)

We present the spine calculus S →−◦& ⊤ as an efficient representation for the linear λ-calculus λ →−◦& ⊤ which includes unrestricted functions (→), linear functions...

A type theory for memory allocation and data layout (2003)

We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic...

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Abstract Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of...

A monadic analysis of information flow security with mutable state (2003)

A modal foundation for meta-variables (2003)

Abstract. We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such...

Ar Nanevski, Brigitte Pientka, Frank Pfenning

Abstract. We report on work in progress regarding a foundation for the notion of meta-variable in logical frameworks and type theories. Our proposal is to treat meta-variables as modal variables in a...

A concurrent logical framework I: Judgments and properties (2003)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

The Concurrent Logical Framework, or CLF, is a new logical framework in which concurrent computations can be represented as monadic objects, for which there is an intrinsic notion of concurrency. It...

ETPS: A System to Help Students Write Formal Proofs (2003)

Chad E. Brown, Peter B. Andrews, Peter B. Andrews, Matthew Bishop, Matthew Bishop, Sunil Issar, ...

ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in rst-order logic or higher-order logic. It enables students to concentrate on the...

A Denotational Approach to Measuring Complexity in Functional Programs (2003)

Kathryn Van Stone, Frank Pfenning

Copyright c○2003 Kathryn Van Stone

CMU-CS-03-131R (2003)

A Bor-yuh, Evan Chang, Kaustuv Chaudhuri, Frank Pfenning

A type theory for memory allocation and data layout (2003)

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Abstract Ordered type theory is an extension of linear type theory in which variables in the context may be neitherdropped nor re-ordered. This restriction gives rise to a natural notion of...

Abstract. We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such...

A learning algorithm for localizing people based on wireless signal strength that uses labeled and unlabeled data (2003)

We present the spine calculus S →−◦& ⊤ as an efficient representation for the linear λ-calculus λ →−◦& ⊤ which includes unrestricted functions (→), linear functions...

Mary Berna, Brennan Sellner, Brad Lisien, Sebastian Thrun, Geoffrey Gordon, Frank Pfenning

This paper summarizes a probabilistic approach for localizing people through the signal strengths of a wireless IEEE 802.11b network. Our approach uses data labeled by ground truth position to learn...

A Type Theory for Memory Allocation and Data Layout (2003)

We present the spine calculus S →−◦& ⊤ as an efficient representation for the linear λ-calculus λ →−◦& ⊤ which includes unrestricted functions (→), linear functions...

Leaf Petersen Robert, Robert Harper, Karl Crary, Frank Pfenning

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...

A Coverage Checking Algorithm for LF (2003)

Carsten Schurmann And, Carsten Schürmann, Frank Pfenning

Coverage checking is the problem of deciding whether any closed term of a given type is an instance of at least one of a given set of patterns. It can be used to verify if a function defined by...

A Judgmental Analysis of Linear Logic (2003)

ETPS: A System to Help Students Write Formal Proofs (2003)

We reexamine the foundations of linear logic, developing a system of natural deduction following Martin-Lof's separation of judgments from propositions. Our construction yields a clean and...

Peter Andrews, Peter B. Andrews, Chad E. Brown, Chad E. Brown, Matthew Bishop, Matthew Bishop, ...

ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...

Walker.A concurrent logical framework: The propositional fragment (2003)

Abstract. We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such...

Kevin Watkins, Iliano Cervesato, Frank Pfenning

, and David Walker 3 1

A Linear Spine Calculus (2003)

Cervesato, Iliano, Pfenning, Frank

We present the spine calculus S→⊸&⊤ as an efficient representation for the linear λ-calculus λ→⊸&⊤ which includes unrestricted functions (→) linear functions (⊸)...

A concurrent logical framework ii: Examples and applications (2002)

Iliano Cervesato, Frank Pfenning, David Walker, Kevin Watkins

CLF is a new logical framework with an intrinsic notion of concurrency. It is designed as a conservative extension of the linear logical framework LLF with the synchronous connectives, 1,!, and of...

A concurrent logical framework I: Judgments and properties (2002)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

The Concurrent Logical Framework, or CLF, is a new logical framework in which concurrent computations can be represented as monadic objects, for which there is an intrinsic notion of concurrency. It...

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to e#ectively tap into the resources available on the global...

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to eectively tap into the resources available on the global...

Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer's Perspective (2002)

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to e#ectively tap into the resources available on the global...

Towards a Functional Library for Fault-Tolerant (2002)

With the vast amount of computing resources distributed throughout the world today, the prospect of e#ectively harnessing these resources has captivated the imaginations of many and motivated both...

Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, ...

To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required.

Trustless Grid Computing in ConCert (2002)

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to e#ectively tap into the resources available on the global network...

Contents (2002)

This material is in rough draft form and is likely to contain errors. Furthermore, citations are in no way adequate or complete. Please do not cite or distribute this document. This work was...

A concurrent logical framework I: Judgments and properties (2002)

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...

Kevin Watkins, Iliano Cervesato, David Walker, Frank Pfenning

“Efficient Logics for Network Security, ” grant N00014-01-1-0432; by DARPA under the title “Scaling Proof-

A concurrent logical framework ii: Examples and applications (2002)

Iliano Cervesato, Frank Pfenning, David Walker, Kevin Watkins

“Efficient Logics for Network Security, ” grant N00014-01-1-0432; by DARPA under the title “Scaling Proof-

A concurrent logical framework ii: Examples and applications (2002)

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...

Iliano Cervesato, Frank Pfenning, David Walker, Kevin Watkins

“Efficient Logics for Network Security, ” grant N00014-01-1-0432; by DARPA under the title “Scaling Proof-

A concurrent logical framework I: Judgments and properties (2002)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

“Efficient Logics for Network Security, ” grant N00014-01-1-0432; by DARPA under the title “Scaling Proof-

Iktara in ConCert: Realizing a certified grid computing framework from a programmer’s perspective (2002)

With the vast amount of computing resources distributed throughout the world today, the prospect of effectively harnessing these resources has captivated the imaginations of many and motivated both...

A concurrent logical framework ii: Examples and applications (2002)

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...

Iliano Cervesato, Frank Pfenning, David Walker, Kevin Watkins

“Efficient Logics for Network Security, ” grant N00014-01-1-0432; by DARPA under the title “Scaling Proof-

Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...

Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...

Contents (2001)

Frank Pfenning, Cop Yrigh

Notes for a course given at Carnegie Mellon University during the Spring semester of 2001. Please send comments tofp@cs.cmu.edu. These notes are to be published by Cambridge University Press....

Please (2001)

Notes for acourse giv en at Carnegie

Logical and Meta-Logical Frameworks (2001)

Frank Pfenning, Marktoberdorf Summer School

• If you play squash see me after lecture!

Human-readable machine-verifiable proofs for teaching constructive logic (2001)

Intensionality, extensionality, and proof irrelevance in modal type theory (2001)

Abstract. A linear syntax for natural deduction proofs in first-order intuitionistic logic is presented, which has been an effective tool for teaching logic. The proof checking algorithm is also...

Human-readable machine-verifiable proofs for teaching constructive logic (2001)

We develop a uniform type theory that integrates intensionality, extensionality, and proof irrelevance as judgmental concepts. Any object may be treated intensionally (subject only to #-conversion),...

Intensionality, extensionality, and proof irrelevance in modal type theory (2001)

Abstract. A linear syntax for natural deduction proofs in first-order intuitionistic logic is presented, which has been an effective tool for teaching logic. The proof checking algorithm is also...

Intensionality, extensionality, and proof irrelevance in modal type theory (2001)

We develop a uniform type theory that integrates intensionality, extensionality, and proof irrelevance as judgmental concepts. Any object may be treated intensionally (subject only to α-conversion),...

A Judgmental Reconstruction of Modal Logic (2001)

We develop a uniform type theory that integrates intensionality, extensionality, and proof irrelevance as judgmental concepts. Any object may be treated intensionally (subject only to ff-conversion),...

Frank Pfenning, I Ng, Rowan Davies, I Es

this paper we reconsider the foundations of modal logic, following Martin-Lof's (1996) methodology of distinguishing judgments from propositions. We give constructive meaning explanations for...

Modal Typing for Specifying Run-time Code Generation (2001)

Geoffrey Washburn, Peter Lee, Frank Pfenning

Syntax Initially the translated code made use of the same abstract syntax modules in representing code as the did compiler/translator. However, eventually due to the complication of reasoning about...

Modularity Matters Most (2001)

Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component parts, but rather the...

Contents (2001)

We present the spine calculusË � Æ�as an efficient representation for the linear�-calculus� � Æ�which includes unrestricted functions (�), linear functions ( Æ), additive...

x (2001)

Modularity Matters, Most Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

Abstract We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component parts, but...

Contents (2001)

Automated Techniques for Provably Safe Mobile Code (2001)

We present the spine calculus S →−◦& ⊤ as an efficient representation for the linear λ-calculus λ →−◦& ⊤ which includes unrestricted functions (→), linear functions...

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....

Generalized Aliasing as a Basis for Program Analysis Tools (2001)

Robert Callahan November, Frank Pfenning, Craig Chambers

Tools for automatic program analysis promise to improve programmer productivity by searching and summarizing large bodies of code. However, the phenomenon of aliasing --- different names being used...

Human-readable machine-verifiable proofs for teaching constructive logic (2001)

• Bi-Directional Type Checking (2001)

Abstract. A linear syntax for natural deduction proofs in first-order intuitionistic logic is presented, which has been an effective tool for teaching logic. The proof checking algorithm is also...

Rowan Davies, Frank Pfenning, Acknowledgments Robertharper

Modal typing for specifying run-time code generation. Available from http://www.cis.upenn.edu/ ∼ geoffw/research (2001)

Geoffrey Washburn, Peter Lee, Frank Pfenning

0.1 Purpose and Motivation One of the classical tradeoffs in the development of software systems involves the choice between abstraction and performance. Abstraction leads to flexible, reusable, and...

Automated Techniques for Provably Safe Mobile Code (2000)

Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy that is attached to a binary....

Automated Techniques for Provably Safe Mobile Code (2000)

Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....

On equivalence and canonical forms in the LF type theory (2000)

Properties of terms in continuation-passing style in an ordered logical framework (2000)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Properties of terms in continuation-passing style in an ordered logical framework (2000)

A logical framework is a meta-language for the formalization of deductive systems as used in the description of logics and programming languages. It should directly support common notions and...

Structural cut elimination I. intuitionistic and classical logic (2000)

A logical framework is a meta-language for the formalization of deductive systems as used in the description of logics and programming languages. It should directly support common notions and...

Automated techniques for provably safe mobile code (2000)

We present new variants of known proofs of cut elimination for intuitionistic and classical sequent calculi. In both cases the proofs proceed by three nested structural inductions, avoiding the...

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....

Termination and Reduction Checking in the Logical Framework (2000)

Automated techniques for provably safe mobile code (2000)

The logical framework LF [HHP93] offers concise encodings of deductive systems and their meta-theory. Twelf [SP98] is a realization of LF. It provides a higher-order logic programming language for...

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....

Efficient Resource Management for Linear Logic Proof Search (2000)

Properties of Terms in Continuation-Passing Style in an Ordered Logical Framework (2000)

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and...

Intersection Types and Computational Effects (2000)

Machine We now begin extending our representation to include evaluation of CPS terms. We will begin by showing a representation of a naive evaluator which makes no use of the ordering invariants. The...

Termination and Reduction Checking in the Logical Framework (2000)

We show that standard formulations of intersection type systems are unsound in the presence of computational effects, and propose a solution similar to the value restriction for polymorphism adopted...

On Equivalence and Canonical Forms (2000)

this paper, we present a reduction and termination checker which reasons about orders. The reduction checker verifies properties relating input and out1 put. The termination checker proves properties...

In The Lf, Robert Harper, Frank Pfenning

this paper we present a new, type-directed equivalence algorithm for the LF type theory that overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richer languages,...

Automated Techniques for Provably Safe Mobile Code (2000)

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....

Termination and Reduction Checking in the Logical Framework (2000)

Under consideration for publication in Math. Struct. in Comp. Science A Judgmental Reconstruction of Modal Logic (2000)

The logical framework LF [HHP93] offers concise encodings of deductive systems

Frank Pfenning, Rowan Davies

We reconsider the foundations of modal logic, following Martin-Löf’s methodology of distinguishing judgments from propositions. We give constructive meaning explanations for necessity and...

On equivalence and canonical forms in the LF type theory (2000)

On equivalence and canonical forms in the LF type theory (2000)

Decidability of de nitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of de nitional equality are...

The Realizability Approach to Computable Analysis and Topology (2000)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Andrej Bauer, Steven M. Awodey, Lenore Blum, Abbas Edalat, Frank Pfenning

policies, either expressed or implied, of the NSF, NAFSA, or the U.S. government.

On equivalence and canonical forms in the LF type theory (2000)

Automated Techniques for Provably Safe Mobile Code (2000)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....

On Equivalence and Canonical Forms intheLFTypeTheory (2000)

On Equivalence and Canonical Forms intheLFTypeTheory (2000)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

• Elimination via subtyping (2000)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

On Equivalence and Canonical Forms (2000)

In The Lf, Robert Harper, Frank Pfenning

this paper we present a new, type-directed equivalence algorithm for the LF type theory that overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richer languages,...

Contents (2000)

2000. Material for this course is available at

Contents (1999)

Material for the course Automated Theorem Proving at Carnegie Mellon University, Fall 1999. This includes revised versions from the course notes on Linear Logic (Spring 1998) and Computation and...

Contents (1999)

A judgmental reconstruction of modal logic (1999)

Material for the course Automated Theorem Proving at Carnegie Mellon University, Fall 1999. This includes revised versions from the course notes on Linear Logic (Spring 1998) and Computation and...

Frank Pfenning, Rowan Davies

In this paper we reconsider the foundations of modal logic, following MartinL of's methodology of distinguishing judgments from propositions [ML85]. We give constructive meaning explanations for...

Dependent Types in Practical Programming (extended abstract (1999)

Ordered Linear Logic Programming (1999)

fpcs.cmu.edu We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C)...

Frank Pfenning, Jeff Polakow, Jeff Polakow

this paper we investigate logic programming with ordered hypotheses. We follow the paradigm that logic programming should be understood via an abstract notion of uniform derivation [MNPS91] which, in...

A Modal Analysis of Staged Computation (1999)

Natural Deduction for Intuitionistic Non-Commutative Linear Logic (1999)

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of typed lambda-calculi and...

Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic (1999)

We present a system of natural deduction and associated term calculus for intuitionistic non-commutative linear logic (INCLL) as a conservative extension of intuitionistic linear logic. We prove...

Dependent Types in Practical Programming (Extended Abstract) (1999)

We present a sequent calculus for intuitionistic non-commutative linear logic (INCLL) , show that it satisfies cut elimination, and investigate its relationship to a natural deduction system for the...

Automated Theorem Proving (1999)

) Hongwei Xi Department of Computer Science and Engineering Oregon Graduate Institute of Science and Technology hongwei@cse.ogi.edu Frank Pfenning Department of Computer Science Carnegie Mellon...

On Equivalence and Canonical Forms in the LF Type Theory (1999)

this document.

Dependent Types in Practical Programming (1999)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Extend Ed, Hongwei Xi, Frank Pfenning

) Hongwei Xi Department of Computer Science and Engineering Oregon Graduate Institute of Science and Technology hongwei@cse.ogi.edu Frank Pfenning Department of Computer Science Carnegie Mellon...

On Equivalence and Canonical Forms in the LF Type Theory (1999)

The Relative Complement Problem for Higher-Order Patterns (1999)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

System Description: Twelf --- A Meta-Logical Framework for Deductive Systems (1999)

We address the problem of complementing higher-order patterns without repetitions of free variables. Differently from the first-order case, the complement of a pattern cannot, in general, be...

Frank Pfenning, Carsten Schurmann

. Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory...

On proving syntactic properties of CPS programs (1999)

The Relative Complement Problem for Higher-Order Patterns (1999)

Higher-order program transformations raise new challenges for proving properties of their output, since they resist traditional, first-order proof techniques. In this work, we consider (1) the...

On proving syntactic properties of CPS programs (1999)

We address the problem of complementing higher-order patterns without repetitions of free variables. Differently from the first-order case, the complement of a pattern cannot, in general, be...

Olivier Danvy, Belmina Dza C, Frank Pfenning

Higher-order program transformations raise new challenges for proving properties of their output, since they resist traditional, rst-order proof techniques. In this work, we consider (1) the...

Strategies in Automated Deduction (STRATEGIES'99) (1999)

Bernhard Gramlich, Hélène Kirchner, Frank Pfenning (eds.)

) . . . . . . . . 33 Didier Galmiche Annotated Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Dieter Hutter An Approach to Flexible Forms of Proof...

On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) (1999)

The Relative Complement Problem for Higher-Order Patterns (1999)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

System Description: Twelf - A Meta-Logical Framework for Deductive Systems (1999)

We address the problem of complementing higher-order patterns without repetitions of free variables. Differently from the first-order case, the complement of a pattern cannot, in general, be...

A Formalization of the Proof-Carrying Code Architecture in a Linear Logical Framework (1999)

. Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory...

Mark Plesko, Frank Pfenning

this paper we formalize the PCC safety architecture in a logical framework, which constitutes an important first step towards an environment for experimentation and formal verification of properties...

Natural Deduction for Intuitionistic Non-Commutative Linear Logic (1999)

Higher-Order Pattern Complement and Strict Lambda-Calculus (1999)

. We present a system of natural deduction and associated term calculus for intuitionistic non-commutative linear logic (INCLL) as a conservative extension of intuitionistic linear logic. We prove...

On Equivalence and Canonical Forms intheLFTypeTheory (1999)

. We address the problem of complementing higher-order linear patterns, i.e. without repetitions of free variables. Differently from the first-order case, the complement of a pattern cannot, in...

A formalization of the proof-carrying code architecture in a linear logical framework (1999)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Mark Plesko, Frank Pfenning

On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) ∗ (1999)

System description: Twelf — A meta-logical framework for deductive systems (1999)

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...

Natural deduction for intuitionistic non-commutative linear logic (1999)

Abstract. Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type...

The relative complement problem for higher-order patterns (1999)

Abstract. We present a system of natural deduction and associated term calculus for intuitionistic non-commutative linear logic (INCLL) as a conservative extension of intuitionistic linear logic. We...

Natural deduction for intuitionistic non-commutative linear logic (1999)

We address the problem of complementing higher-order patterns without repetitions of free variables. Differently from the first-order case, the complement of a pattern cannot, in general, be...

On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) (1999)

Abstract. We present a system of natural deduction and associated term calculus for intuitionistic non-commutative linear logic (INCLL) as a conservative extension of intuitionistic linear logic. We...

The relative complement problem for higher-order patterns (1999)

Decidability of de nitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of de nitional equality are...

This document in subdirectoryRS/99/23/ On proving syntactic properties of CPS programs ∗ (1999)

We address the problem of complementing higher-order patterns without repetitions of free variables. Di erently from the rst-order case, the complement of a pattern cannot, in general, be described...

Olivier Danvy, Belmina Dzafic, Frank Pfenning, Copyright C, Olivier Danvy, Belmina Dzafic, ...

Basic Research in Computer Science

Unification via Explicit Substitutions: The Case of Higher-Order Patterns (1998)

Dowek, Gilles, Hardin, Thérèse, Kirchner, Claude, Pfenning, Frank

In [6] we have proposed a general higher-order unification method using a theory of explicit substitutions and we have proved its completeness. In this paper, we investigate the case of higher-order...

Contents (1998)

Ordered Linear Logic Programming (1998)

This material is in rough draft form and is likely to contain errors. Furthermore, citations are in no way adequate or complete. Please do not cite or distribute this document. This work was...

Unification via Explicit Substitutions: The Case of Higher-Order Patterns (1998)

We begin with a review of intuitionistic non-commutative linear logic (INCLL), a refinement of linear logic with an inherent notion of order proposed by the authors in prior work. We then develop a...

Therese Hardin, Gilles Dowek, Gilles Dowek, Claude Kirchner, Claude Kirchner, Frank Pfenning, ...

In [6] we have proposed a general higher-order unification method using a theory of explicit substitutions and we have proved its completeness. In this paper, we investigate the case of higher-order...

Automated Theorem Proving in a Simple Meta-Logic for LF (1998)

Carsten Schurmann And, Carsten Schurmann, Frank Pfenning

. Higher-order representation techniques allow elegant encodings of logics and programming languages in the logical framework LF, but unfortunately they are fundamentally incompatible with induction...

Modal Types as Staging Specifications for Run-time Code Generation (1998)

Philip Wickline, Peter Lee, Frank Pfenning, Rowan Davies

ing with credit is permitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works, requires prior specific permission...

Algorithms for Equality and Unification in the Presence of Notational Definitions (1998)

Automated Theorem Proving in a Simple Meta Logic for LF (1998)

this paper we investigate the interaction of notational definitions with algorithms for testing equality and unification. We propose a syntactic criterion on definitions which avoids their expansion...

Eliminating Array Bound Checking Through Dependent Types (1998)

. Higher-order representation techniques allow elegant encodings of logics and programming languages in the logical framework LF, but unfortunately they are fundamentally incompatible with induction...

Algorithms for Equality and Unification in the Presence of Notational Definitions (1998)

We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the...

Frank Pfenning And, Frank Pfenning, Carsten Schurmann

this paper we investigate the interaction of notational definitions with algorithms for testing equality and unification. We propose a syntactic criterion on definitions which avoids their expansion...

Run-time Code Generation and Modal-ML (1998)

Philip Wickline, Peter Lee, Frank Pfenning

This paper presents early experience with a typed programming language and compiler for run-time code generation. The language is an extension of the SML language with modal operators, based on the 2...

The Fox Project: Advanced Language Technology for Extensible Systems (1998)

Robert Harper, Peter Lee, Frank Pfenning

It has been amply demonstrated in recent years that careful attention to the structure of systems software can lead to greater flexibility, reliability, and ease of implementation, without incurring...

Run-time Code Generation and Modal-ML (1998)

Philip Wickline, Peter Lee, Frank Pfenning

This paper presents a typed programming language and compiler for run-time code generation. The language, called ML 2 , extends ML with modal operators in the style of the Mini-ML 2 e language of...

Ordered Linear Logic Programming (1998)

Jeff Polakow, Frank Pfenning, Frank Pfenning

this paper we investigate logic programming with ordered hypotheses. We follow the paradigm that logic programming should be understood via an abstract notion of uniform derivation [MNPS91] which, in...

Algorithms for Equality and Unification in the Presence of Notational Definitions (1998)

Frank Pfenning, Carsten Schurmann

this paper we investigate the interaction of notational definitions with algorithms for testing equality and unification. We propose a syntactic criterion on definitions which avoids their expansion...

Automated Theorem Proving in a Simple Meta Logic for LF (1998)

Algorithms for Equality and Unification in the Presence of Notational Definitions (1998)

. Higher-order representation techniques allow elegant encodings of logics and programming languages in the logical framework LF, but unfortunately they are fundamentally incompatible with induction...

Modal Types as Staging Specifications for Run-Time Code Generation (1998)

this paper we investigate the interaction of notational definitions with algorithms for testing equality and unification. We propose a syntactic criterion on definitions which avoids their expansion...

Philip Wickline, Peter Lee, Frank Pfenning, Rowan Davies

Runtime code generation has been shown to be a powerful technique for exploiting specialization opportunities in many programs. We propose the use of sourcelevel annotations from a modal...

Ordered linear logic programming (1998)

Je Polakow, Frank Pfenning

We begin with a review of intuitionistic non-commutative linear logic (INCLL), a re nement of linear logic with an inherent notion of order proposed by the authors in prior work. We then develop a...

Ordered linear logic programming (1998)

The Fox project: Advanced language technology for extensible systems (1998)

We begin with a review of intuitionistic non-commutative linear logic (INCLL), a refinement of linear logic with an inherent notion of order proposed by the authors in prior work. We then develop a...

Robert Harper, Peter Lee, Frank Pfenning

should not be interpreted as representing official policies, either expressed or implied, of

Automated theorem proving in a simple meta-logic for LF (1998)

Algorithms for equality and unification in the presence of notational definitions (1998)

Abstract. Higher-order representation techniques allow elegant encodings of logics and programming languages in the logical framework LF, but unfortunately they are fundamentally incompatible with...

Ordered linear logic programming (1998)

Frank Pfenning, Jeff Polakow, Jeff Polakow

Webeginwithareviewofordered linear logic (OLL) 1, a refinement of linear logic with an inherent notion of order proposed by the authors in prior work. We then develop a logic programming...

A Module System for a Programming Language Based on the LF Logical Framework (1998)

HARPER, ROBERT, PFENNING, FRANK

We describe a module system for Elf, a logic programming language based on the LF logical framework. The static part of the module calculus addresses name-space management and structured presentation...

We present the spine calculus S #-#& # as an efficient representation for the linear #-calculus # #-#& # which includes unrestricted functions (#), linear functions (-#), additive pairing...

We present the spine calculus S as an efficient representation for the linear -calculus which includes unrestricted functions (!), linear functions (), additive pairing (&), and additive unit...

We develop an efficient representation and a pre-unification algorithm in the style of Huet for the linear

We develop an efficient representation and a preAppeared

We develop a pre-unification algorithm in the style of Huet for the linear-calculus!\Gammaffi&? which includes intuitionistic functions (!), linear functions (\Gammaffi), additive pairing...

Practical refinement-type checking (1997)

We present the spine calculus S as an efficient representation for the linear -calculus which includes unrestricted functions (!), linear functions (), additive pairing (&), and additive unit...

Efficient Resource Management for Linear Logic Proof Search (1997)

Refinement types allow many more properties of programs to be expressed and statically checked than conventional type systems. We present a practical algorithm for refinement-type checking in...

Linear Higher-Order Pre-Unification (1997)

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and...

Linear Higher-Order Pre-Unification (1997)

We develop an efficient representation and a preThis extended abstract has been accepted at the Twelfth Annual Symposium on Logic in Computer Science - LICS'97, Warsaw, Poland, June 29th -- July...

A Schema for Adding Dependent Types to ML (1997)

We develop a pre-unification algorithm in the style of Huet for the linear -calculus !\Gammaffi&? which includes intuitionistic functions (!), linear functions (\Gammaffi), additive pairing...

A Linear Spine Calculus (1997)

We present an approach to enriching the type system of ML with a form of dependent types, where index objects are restricted to constraint domains C, leading to the DML(C) language schema. Pure...

Iliano Cervesato And, Iliano Cervesato, Frank Pfenning

We present the spine calculus S !\Gammaffi&? as an efficient representation for the linear -calculus !\Gammaffi&? which includes intuitionistic functions (!), linear functions (\Gammaffi),...

Computation and Deduction (1997)

Frank Pfenning Carnegie, Frank Pfenning

Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3 Operational Semantics . . . . . . . . . . ....

A Schema for Adding Dependent Types to ML (1997)

Computation and Deduction (1997)

We present an approach to enriching ML's type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure...

Practical Refinement-Type Checking (1997)

Syntax : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 2.2 Substitution : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 10 2.3 Operational Semantics : : : : : : : : : : :...

Computation and Deduction (1997)

Refinement types allow many more properties of programs to be expressed and statically checked than conventional type systems. We present a practical algorithm for refinement-type checking in a...

Compiling with Proofs (1997)

Syntax : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 2.2 Substitution : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 10 2.3 Operational Semantics : : : : : : : : : : :...

George C. Necula, Robert Harper, Frank Pfenning

I propose a new compiler architecture for compiling source-level programs into a combination of object code and a proof that the object code preserves certain properties of the source program. Such a...

We present the spine calculus S →−◦& ⊤ as an efficient representation for the linear λ-calculus λ →−◦&⊤ which includes intuitionistic functions (→), linear functions...

Primitive Recursion for Higher-Order Abstract Syntax (1997)

We develop a pre-unification algorithm in the style of Huet for the linear λ-calculus λ →−◦& ⊤ which includes intuitionistic functions (→), linear functions (−◦), additive pairing...

Joëlle Despeyroux, Frank Pfenning

Abstract (1997)

Practical refinement-type checking (1997)

We present an approach to enriching ML’s type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure...

Primitive Recursion for Higher-Order Abstract Syntax (1997)

Technical summary submitted to POPL’98 ∗

1 Introduction Higher-order abstract syntax is a central representation technique in many logical frameworks, that is, meta-languages designed for the formalization of deductive systems. The basic...

We develop an efficient representation and a pre-unification algorithm in the style of Huet for the linear λ-calculus λ →−◦& ⊤ which includes intuitionistic functions (→), linear...

Contents (1997)

Efficient resource management for linear logic proof search (1996)

Draft notes for a course given at Carnegie Mellon University during the fall semester

Iliano Cervesato, Joshuas. Hodas, Frank Pfenning

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and...

A linear logical framework (1996)

A linear logical framework (1996)

We present the linear type theory LLF as the forAppeared

We present the linear type theory \Pi\Gammaffi&? as the formal basis for LLF, a conservative extenSubmitted to Information & Computation. Comments are welcome! sion of the logical framework...

Also published as FOX Memorandum CMU-CS-FOX-95-02 We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation...

Also published as FOX Memorandum CMU-CS-FOX-99-02 We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation...

A Modal Analysis of Staged Computation (1996)

syntax Concrete syntax Kinds type type \Pix : A: K --x:AK A -? K K !- A P M P M ? !T? Types A&B A & B A \Gammaffi B A -o B B o- A \Pix : A: B --x:AB A -? B B !- A hi () hM; Ni M,N fst M !fst?...

Unification via Explicit Substitutions: The Case of Higher-Order Patterns (1996)

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main...

Gilles Dowek, Therese Hardin, Le Chesnay Cedex, Place Jussieu, Claude Kirchner, Frank Pfenning

Following the general method and related completeness results on using explicit substitutions to perform higher-order unification proposed in [5], we investigate in this paper the case of...

The Practice of Logical Frameworks (1996)

Introduction Deductive systems, given via axioms and rules of inference, are a common conceptual tool in mathematical logic and computer science. They are used to specify many varieties of logics and...

Mode and Termination Checking for Higher-Order Logic Programs (1996)

We present the linear type theory LLF as the forThis extended abstract will appear on the proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science --- LICS'96, New...

Ekkehard Rohwedder, Frank Pfenning

. We consider how mode (such as input and output) and termination properties of typed higher-order constraint logic programming languages may be declared and checked effectively. The systems that we...

A Modal Analysis of Staged Computation (1996)

We present the linear type theory \Pi\Gammaffi&? as the formal basis for LLF, a conservative extenSubmitted to Information & Computation. Comments are welcome! sion of the logical framework...

A Modal Analysis of Staged Computation (1996)

ing with credit is permitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works, requires prior specific permission...

Rowan Davies And, Rowan Davies, Frank Pfenning

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main...

Linear Higher-Order Pre-Unification (Extended Abstract) (1996)

We present the linear type theory \Pi\Gammaffi&? as the formal basis for LLF, a conservative extenSubmitted to Information & Computation. Comments are welcome! sion of the logical framework...

Unification via Explicit Substitutions: The Case of Higher-Order Patterns (1996)

We develop an efficient representation and a pre-unification algorithm in the style of Huet for the This extended abstract has been submitted to the CADE-13 Workshop on Proof Search in Type-Theoretic...

Gilles Dowek, Therese Hardin, Le Chesnay Cedex, Place Jussieu, Claude Kirchner, ...

Following the general method and related completeness results on using explicit substitutions to perform higher-order uniøcation proposed in [5], we investigate in this paper the case of...

Abstract (1996)

Efficient resource management for linear logic proof search (1996)

Continuation-passing style (CPS) is often criticized to be more expensive than the usual direct style of functional programming. By structure, CPS functions indeed are passed one extra argument (the...

Iliano Cervesato, Joshuas. Hodas, Frank Pfenning

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and...

Mode and termination checking for higher-order logic programs (1996)

Ekkehard Rohwedder, Frank Pfenning

Abstract. We consider how mode (such as input and output) and termination properties of typed higher-order constraint logic programming languages may be declared and checked effectively. The systems...

A linear logical framework (1996)

Also published as FOX Memorandum CMU-CS-FOX-99-02 We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation...

Efficient resource management for linear logic proof search (1996)

Primitive recursion for higher order abstract syntax (1996)

Abstract. The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses...

Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann

Higher-order abstract syntax is a central representation technique in logical frameworks which maps variables of the object language into variables in the meta-language. It leads to concise...

tps: A theorem proving system for classical type theory (1996)

Also published as FOX Memorandum CMU-CS-FOX-99-02 We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation...

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi

This is a description of TPS, a theorem proving system for classical type theory (Church’s typed λ-calculus). TPS has been designed to be a general research tool for manipulating wffs of first-...

Sequent Calculi (1995)

Structural Cut Elimination (1995)

this document. Contents

The Occurrence of Continuation Parameters in CPS Terms (1995)

We present new proofs of cut elimination for intuitionistic, classical, and linear sequent calculi. In all cases the proofs proceed by three nested structural inductions, avoiding the explicit use of...

Olivier Danvy, Frank Pfenning

We prove an occurrence property about formal parameters of continuations in Continuation-Passing Style (CPS) terms that have been automatically produced by CPS transformation of pure, call-byvalue...

The Occurrence of Continuation Parameters in CPS Terms (1995)

Olivier Danvy Frank, Frank Pfenning

We prove an occurrence property about formal parameters of continuations in Continuation-Passing Style (CPS) terms that have been automatically produced by CPS transformation of pure, call-byvalue...

A Modal Analysis of Staged Computation (1995)

The Occurrence of Continuation Parameters in CPS Terms (1995)

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main...

Olivier Danvy, Frank Pfenning

We prove an occurrence property about formal parameters of continuations in Continuation-Passing Style (CPS) terms that have been automatically produced by CPS transformation of pure, call-byvalue...

A compilation manager for standard ML of New Jersey (1994)

Robert Harper, Frank Pfenning, Peter Lee, Eugene Rollins

The design and implementation of a compilation manager (CM) for Standard ML of New Jersey (SML/NJ) is described. Truly independent compilation is difficult to implement correctly and efficiently for...

Structural cut elimination in linear logic (1994)

Elf: A Meta-Language for Deductive Systems (System Description) (1994)

We present a new proof of cut elimination for linear logic which proceeds by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent...

Structural Cut Elimination in Linear Logic (1994)

ce describing the Elf language is [10]. Gentler introductions can be found in [12] and [6]. Elf has also been used in a graduate course on the theory of programming languages. A draft of the course...

Incremental Recompilation for Standard ML of New Jersey (1994)

We present a new proof of cut elimination for linear logic which proceeds by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent...

Robert Harper Frank, Frank Pfenning, Peter Lee, Eugene Rollins

The design and implementation of an incremental recompilation manager (IRM) for Standard ML of New Jersey (SML/NJ) is described. Truly separate compilation is difficult to implement correctly and...

TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory (1994)

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi, ...

This is a demonstration of TPS, a theorem proving system for classical type theory (Church's typed l-calculus). TPS can be used interactively or automatically, or in a combination of these...

A Structural Proof of Cut Elimination and Its Representation in a Logical Framework (1994)

A Structural proof of cut elimination and its representation in a logical framework (1994)

We present new proofs of cut elimination for intuitionistic and classical sequent calculi. In both cases the proofs proceed by three nested structural inductions, avoiding the explicit use of...

Elf: A meta-language for deductive systems (system description (1994)

We present new proofs of cut elimination for intuitionistic and classical sequent calculi. In both cases the proofs proceed by three nested structural inductions, avoiding the explicit use of...

2 CLL: A Traditional Sequent Calculus for Linear Logic 1 (1994)

Elf is a uniform meta-language for the formalization of the theory of programming languages and logics. It provides means for 1. specifying the abstract syntax and semantics of an object language in...

TPS: A Theorem Proving System for Classical Type Theory (1994)

We present a new proof of cut elimination for linear logic which proceeds by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent...

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi

This is a description of TPS, a theorem proving system for classical type theory (Church's typed l-calculus). TPS has been designed to be a general research tool for manipulating wffs of first-...

Refinement Types for Logical Frameworks (1993)

Higher-Order Logic Programming as Constraint Logic Programming (1993)

We propose a refinement of the type theory underlying the LF logical framework by a form of subtypes and intersection types. This refinement preserves desirable features of LF, such as decidability...

Refinement types for logical frameworks (1993)

Higher-order logic programming (HOLP) languages are particularly useful for various kinds of metaprogramming and theorem proving tasks because of the logical support for variable binding via -...

Higher-order logic programming as constraint logic programming (1993)

We propose a refinement of the type theory underlying the LF logical framework by a form of subtypes and intersection types. This refinement preserves desirable features of LF, such as decidability...

Refinement types for logical frameworks (1993)

Higher-order logic programming (HOLP) languages are particularly useful for various kinds of metaprogramming and theorem proving tasks because of the logical support for variable binding via...

On the undecidability of partial polymorphic type reconstruction (1993)

We propose a refinement of the type theory underlying the LF logical framework by a form of subtypes and intersection types. This refinement preserves desirable features of LF, such as decidability...

Unification in a λ-calculus with intersection types (1993)

We prove that partial type reconstruction for the pure polymorphic λ-calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J. Boehm. We...

Michael Kohlhase, Frank Pfenning

We propose related algorithms for unification and constraint simplification in λ → & , a refinement of the simply-typed λ-calculus with subtypes and bounded intersection types. λ → &...

An Empirical Study of the Runtime Behavior of Higher-Order Logic Programs (1992)

Implementing the Meta-Theory of Deductive Systems (1992)

this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government.

Frank Pfenning, Ekkehard Rohwedder

. We exhibit a methodology for formulating and verifying metatheorems about deductive systems in the Elf language, an implementation of the LF Logical Framework with an operational semantics in the...

On the Undecidability of Partial Polymorphic Type Reconstruction (1992)

A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework (1992)

We prove that partial type reconstruction for the pure polymorphic -calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J. Boehm. We...

Compiler Verification in LF (1992)

We give a detailed, informal proof of the Church-Rosser property for the untyped lambda-calculus and show its representation in LF. The proof is due to Tait and Martin-Löf and is based on the notion...

John Hannan, Frank Pfenning

We sketch a methodology for the verification of compiler correctness based on the LF Logical Framework as realized within the Elf programming language. We have applied this technique to specify,...

On the Undecidability of Partial Polymorphic Type Reconstruction (1992)

Frank Pfenning January, Frank Pfenning

We prove that partial type reconstruction for the pure polymorphic -calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J. Boehm. We...

A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework (1992)

Frank Pfenning September, Frank Pfenning

We give a detailed, informal proof of the Church-Rosser property for the untyped -calculus and show its representation in LF. The proof is due to Tait and Martin-Lof and is based on the notion of...

Intersection Types for a Logical Framework (1992)

The Type System of a Higher-Order Logic Programming Language (1992)

We propose a refinement of the type theory underlying the LF logical framework by a form of subtypes and intersection types. This refinement preserves desirable features of LF, such as decidability...

Gopalan Nadathur, Gopalan Nadathur, Frank Pfenning, Frank Pfenning

this paper is to discuss another important but somewhat less exposed component of the language, namely its type system. The traditional purpose of types in programming languages has been to provide...

Implementing the Meta-Theory of Deductive Systems (1992)

Frank Pfenning, Ekkehard Rohwedder

Abstract. We exhibit a methodology for formulating and verifying metatheorems about deductive systems in the Elf language, an implementation of the LF Logical Framework with an operational semantics...

A proof of the Church-Rosser theorem and its representation in a logical framework (1992)

Rowan Davies, Frank Pfenning, Acknowledgments Robertharper

We give a detailed, informal proof of the Church-Rosser property for the untyped λ-calculus and show its representation in LF. The proof is due to Tait and Martin-Löf and is based on the notion of...

B-method Overview (1992)

On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 199? To appear. Preliminary version available as (1992)

A declarative alternative to "assert" in logic programming (1991)

Abstract We prove that partial type reconstruction for the pure polymorphic *-calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J....

Scott Dietzen, Frank Pfenning

The problem with the standard means by which Prolog programs are extended--- assert--- is that the construct is not semantically well-behaved. A more elegant alternative (adopted, for example, in...

A declarative alternative to assert in logic programming (1991)

Scott Dietzen, Frank Pfenning

The problem with the standard means by which Prolog programs are extended — assert — is that the construct is not semantically well-behaved. A more elegant alternative (adopted, for example, in...

A Semi-Functional Implementation of a Higher-Order Logic Programming Language (1991)

Conal Elliott, Frank Pfenning

ions *) and varbind = Varbind of string * term (* Variable binders , Type *) In the implementation of the term language and the type checker, we have two constants type and pi. And, yes, type is a...

Natural Semantics and Some of its Meta-Theory in Elf (1991)

Spiro Michaylov, Frank Pfenning, Im Stadtwald

Operational semantics provide a simple, high-level and elegant means of specifying interpreters for programming languages. In natural semantics, a form of operational semantics, programs are...

Logic Programming in the LF Logical Framework (1991)

Refinement Types for ML (1991)

this paper we describe Elf, a meta-language intended for environments dealing with deductive systems represented in LF. While this paper is intended to include a full description of the Elf core...

Tim Freeman, Frank Pfenning

We describe a refinement of ML's type system allowing the specification of recursively defined subtypes of user-defined datatypes. The resulting system of refinement types preserves desirable...

Unification and Anti-Unification in the Calculus of Constructions (1991)

Modularity in the LF Logical Framework (1991)

We present algorithms for unification and antiunification in the Calculus of Constructions, where occurrences of free variables (the variables subject to instantiation) are restricted to higher-order...

Logic programming in the LF logical framework (1991)

this paper we make a concrete proposal for a module system for the Elf language which attempts to address those three central issues. Various approaches to the static and dynamic semantics of such a...

Modularity in the LF Logical Framework (1991)

Natural semantics and some of its meta-theory in Elf (1991)

Formal deductive systems play an important role in computer science, particularly in the areas of logic and semantics of programming languages. They are employed in three different, but obviously...

A Semi-Functional Implementation of a Higher-Order Logic Programming Language (1990)

Operational semantics provide a simple, high-level and elegant means of specifying interpreters for programming languages. In natural semantics, a form of operational semantics, programs are...

Conal Elliott, Frank Pfenning

ions *) and varbind = Varbind of string * term (* Variable binders , Type *) 30 In the implementation of the term language and the type checker, we have two constants type and pi. And, yes, type is a...

Inductively defined types in the calculus of constructions (1990)

Frank Pfenning, Christine Paulin-mohring

We define the notion of an inductively defined type in the Calculus of Constructions and show how inductively defined types can be represented by closed types. We show that all primitive recursive...

Towards a Practical Programming Language Based on the Polymorphic Lambda Calculus (1989)

Peter Lee, Mark Leone, Spiro Michaylov, Frank Pfenning

The value of polymorphism in programming languages has been demonstrated by languages such as ML [19]. Recent efficient implementations of ML have shown that a language with implicit polymorphism can...

On the Unification Problem for Cartesian Closed Categories (Extended Abstract) (1989)

P. Narendran, Paliath Narendran, Frank Pfenning, Richard Statman

) Paliath Narendran Institute of Programming and Logics Department of Computer Science State University of NY at Albany Albany, NY 12222 dran@cs.albany.edu Frank Pfenning Department of Computer...

Elf: A Language for Logic Definition and Verified Metaprogramming (1989)

UNIFORM PROOFS AS A FOUNDATION FOR LOGIC PROGRAMMING (1989)

We describe Elf, a metalanguage for proof manipulation environments that are independent of any particular logical system. Elf is intended for meta-programs such as theorem provers, proof...

Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov

A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the...

Intersection Types and Computational Effects