| A Concurrent Logical Framework II: Examples and Applications |
MAY 2003 |
86 pages |
| Authors:
Iliano Cervesato; Frank Pfenning; David Walker; Kevin Watkins; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
 | 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 (circle multiply, 1 !, and there exists) of intuitionistic linear logic, encapsulated in a monad. LLF is itself a conservative extension of LF with the asynchronous connectives (logical negation, & and T). In this report, the second of two technical reports ... |
|
| A Concurrent Logical Framework I: Judgments and Properties |
MAY 2003 |
41 pages |
| Authors:
Kevin Watkins; Iliano Cervesato; Frank Pfenning; David Walker; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| 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 is designed as a conservative extension of the linear logical framework LLF with the synchronous connectives (circle multiply, 1, !, and there exists) of intuitionistic linear logic, encapsulated in a monad. LLF is itself a conservative extension of LF ... |
|
| A Current Logical Framework: The Propositional Fragment |
2003 |
|
| Authors:
Kevin Watkins; Iliano Cervesato; Frank Pfenning; David Walker; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
 | We present the propositional fragment CLF of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations in an object language. The underlying type theory uses monadic types to segregate values from computations. This separation leads to a tractable notion of definitional equality that identifies computations differing only in the order of execution of independent steps. From a logical point of ... |
|
| On Equivalence and Canonical Forms in the LF Type Theory |
10 JUL 2000 |
41 pages |
| Authors:
Robert Harper; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| 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 are based on a confluent, strongly-normalizing notion of reduction. Coquand has considered a different approach, directly proving the correctness of a practical equivalence algorithm based on the shape of terms. Neither approach appears to scale well to ... |
|
| A Modal Analysis of Staged Computation |
AUG 1999 |
|
| Authors:
Rowan Davies; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| 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 functional languages. We directly demonstrate the sense in which our calculus captures staging, and also give a conservative embedding of Nielson and Nielson's two level functional language in our language, thus proving that binding time correctness is equivalent to ... |
|
| Logical Frameworks |
1999 |
85 pages |
| Authors:
Frank Pfenning; ELSEVIER SCIENCE PUBLISHERS LTD BARKING(UNITED KINGDOM)
|
| 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 logical theories as well as aspects of programming languages such as type systems or operational semantics. A logical framework is a meta-language for the specification of deductive systems. A number of different frameworks have been proposed and implemented for a ... |
|
| Ordered Linear Logic Programming |
22 DEC 1998 |
35 pages |
| Authors:
Jeff Polakow; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| 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 logic programming interpretation for INCLL in two steps: (1) we give a system of ordered uniform derivations which is sound and complete with respect to INCLL, and (2) we present a model of resource consumption ... |
|
| Twelf User's Guide Version 1.2 |
13 NOV 1998 |
|
| Authors:
Frank Pfenning; Carsten Schuermann; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| This user's guide describes the current version of a succession of implementations of the logical framework LF. It documents the syntax, term reconstruction, and operational semantics already available in an earlier implementation called Elf. The new features described here include a mode checker, a termination checker, an experimental theorem prover for verifying properties of Elf programs, and an Emacs interface. |
|
| The Fox Project: Advanced Language Technology for Extensible Systems |
JAN 1998 |
27 pages |
| Authors:
Robert Harper; Peter Lee; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| 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 an undue penalty in performance. It is our contention that advanced programming languages particularly languages with a mathematically rigorous semantics, and featuring higher-order functions, polymorphic types, and a strong module system are ideally suited ... |
|
| Run-time Code Generation and Modal-ML |
JAN 1998 |
15 pages |
| Authors:
Philip Wickline; Peter Lee; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This paper presents early experience with a typed programming language and compiler for runtime code generation. The language is an extension of the SML language with modal operators, based on the lambda(square) language of Davies and Pfenning. It allows programmers to specify precisely, through types, the stages of computation in a program. The compiler generates target code that makes use of runtime code generation in order to exploit the staging ... |
|
| Linear Higher-Order Pre-Unification |
20 JUL 97 |
|
| Authors:
Iliano Cervesato; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| We develop a pre-unification algorithm in the style of Huet for the linear lambda-calculus lambda(->-o&T) which includes intuitionistic functions (- >) linear functions (-o) additive pairing (&), and additive unit (T). This procedure conveniently operates on an efficient representation of lambda(->-o&T) the spine calculus S(->-o&T) for which we define the concept of weak head-normal form. We prove the soundness and completeness of our algorithm with respect to the proper notion ... |
|
| A Linear Spine Calculus |
10 APR 97 |
|
| Authors:
Iliano Cervesato; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| We present the spine calculus S(approaches -o&T) as an efficient representation for the linear lambda-calculus lambda(approaches -o&T) which includes intuitionistic functions (approach) Tau linear functions (-o)Tau additive pairing (&Tau) and additive unit (T). S(approaches -o&T) enhances the representation of Church's simply typed lamda-calculus as abstract Bolum trees by enforcing extensionality and by incorporating linear constructs. This approach permits procedures such as unification to retain the efficient head access that characterizes ... |
|
| Primitive Recursion for Higher Order Abstract Syntax |
30 AUG 96 |
|
| Authors:
Joelle Despeyroux; Frank Pfenning; Carsten Schurmann; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| 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 encodings, but is incompatible with functions defined by primitive recursion or proofs by induction. In this paper we propose an extension of the simply-typed lambda-calculus with iteration and case constructs which preserves the adequacy of higher-order abstract syntax encodings. The well-known paradoxes ... |
|
| A Modal Analysis of Staged Computation |
MAY 95 |
|
| Authors:
Rowan Davies; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| 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 technical result is a conservative embedding of Nielson & Nielson's two-level functional language in our language Mini-ML, which in addition to partial evaluation also supports multiple computation stages, sharing of code across multiple stages, and run- time code generation. ... |
|
| The Occurrence of Continuation Parameters in CPS Terms |
FEB 95 |
|
| Authors:
Olivier Danvy; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| 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-by-value lamda-terms. Essentially, parameters of continuations obey a stack-like discipline. This property was introduced, but not formally proven, in an earlier work on the Direct-Style transformation (the inverse of the CPS transformation). The proof has been implemented in Elf, a constraint logic programming language based ... |
|
| Structural Cut Elimination in Linear Logic |
DEC 94 |
64 pages |
| Authors:
Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| 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 derivations. The computational content of this proof is a non-deterministic algorithm for cut elimination which is amenable to an elegant implementation in Elf. We show this implementation in detail. (AN) |
|
| A Structural Proof of Cut Elimination and Its Representation in a Logical Framework |
NOV 94 |
68 pages |
| Authors:
Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| 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 multi- sets and termination measures on sequent derivations. This makes them amenable to elegant and concise representations in LF, which are given in full detail. |
|
| A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework |
SEP 92 |
|
| Authors:
Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| We give a detailed, informal proof of the Church-Rosser property for the untyped A-calculus and show its representation in LF. The proof is due to Tait and Martin-L6f and is based on the notion of parallel reduction. The representation employs higher-order abstract syntax and the judgments-as-types principle and takes advantage of term reconstruction as it is provided in the Elf implementation of LF. Proofs of meta-theorems are represented as higher- ... |
|
| A Module System for a Programming Language Based on the LF Logical Framework |
SEP 92 |
|
| Authors:
Robert Harper; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| We describe a module system for Elf, a logic programming language based on the LF logical framework. The static part of module calculus addresses name-space management and structured presentation of deductive systems. The dynamic part addresses search-space management and modularization of logic programs. |
|
Reports by Author
