data structure (abstract of invited lecture). In Fritz Henglein, (2009)
Bill Roscoe, Jim Woodcock, Peter W. O’hearn, John C. Reynolds, ...
[2] Rodney M. Burstall. Some techniques for proving correctness of programs
Keywords: Semantics, Continuation, Continuation-Passing Style (2009)
John C. Reynolds, A. Van Wijngaarden, A. W. Mazurkiewicz, F. L. Morris, C. P. Wadsworth, J. H. Morris, ...
Abstract. We give a brief account of the discoveries of continuations and related concepts
Report of a Workshop on Future Directions in Programming Languages and Compilers (2007)
May Purpose In, Robert Cartwright, Gilles Kahn Inria, Sophia Antipolis, Bernard Lang Inria, James Mcgraw, ...
This paper is the report of their findings. Its purposes are to explain the need for, and benefits of, research in this field--- both basic and applied; to broadly survey the various parts of the...
Types, Abstraction, and Parametric Polymorphism, Part 2 (2007)
Qingming Ma And, Ed. S. Brookes, M. Main, A. Melton, M. Mislove, D. A. Schmidt, ...
ion, and Parametric Polymorphism, Part 2 # QingMing Ma and John C. Reynolds School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890, USA qingming.ma@cs.cmu.edu...
Report of a Workshop on Future Directions in Programming Languages and Compilers (2007)
May Purpose, Robert Cartwright, Gilles Kahn Inria, Sophia Antipolis, Bernard Lang Inria, James Mcgraw, ...
This paper is the report of their findings. Its purposes are to explain the need for, and benefits of, research in this field--- both basic and applied; to broadly survey the various parts of the...
Seoul National University (2007)
Peter W. O'hearn, Queen Mary, Hongseok Yang, John C. Reynolds, Carnegie Mellon
We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from...
Robert Cartwright, Gilles Kahn Inria, Sophia Antipolis, Bernard Lang Inria, James Mcgraw, Lawrence Livermore, ...
In January, 1993, a panel of experts in the area of programming languages and compilers met in a one and a half day workshop to discuss the future of research in that area. This paper is the report...
John C. Reynolds, Peter W. O'hearn, Heap Faults
Extention of Hoare logic for imperative programs Store/heap dichotomy Heap-manipulation commands (not expressions) Independent conjuction ( )
John C. Reynolds, Peter W. O'hearn, Hongseok Yang
The topic of these lectures is an extension of Hoare logic [1, 2] to the specication and proof of programs in which data structures can contain several pointers to the same location, whose contents...
John C. Reynolds, Peter W. O'hearn
ffl Extention of Hoare logic for imperative programs ffl Store/heap dichotomy ffl Heap-manipulation commands (not expressions) ffl Independent conjunction ( ) ffl Unrestricted address arithmetic ffl...
a draft of an article to appear in "Essays on Programming Methodology", edited by A. McIver and C. Morgan, to be published by Springer-Verlag. Copies must not be offered for sale....
An overview of separation logic (2005)
Abstract. After some general remarks about program verification, we introduce separation logic, a novel extension of Hoare logic that can strengthen the applicability and scalability of program...
Local Reasoning about a Copying Garbage Collector (2004)
Lars Birkedal, Noah Torp-smith, John C. Reynolds
We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage...
Separation and Information Hiding (2004)
Peter W. O'Hearn, Hongseok Yang, John C. Reynolds, Peter W. O’hearn, Queen Mary
We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from...
Toward a Grainless Semantics for Shared-Variable Concurrency (2004)
Abstract. Conventional semantics for shared-variable concurrency suffers from the “grain of time ” problem, i.e., the necessity of specifying a default level of atomicity. We propose a semantics...
Local reasoning about a copying garbage collector (2004)
Noah Torp-smith, Lars Birkedal, John C. Reynolds
We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying...
Correctness of a garbage collector via local reasoning (2003)
Lars Birkedal, Lars Birkedal, John C. Reynolds, John C. Reynolds, John C. Reynolds, Noah Torp-smith, ...
All rights reserved. Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.
Separation logic: A logic for shared mutable data structures (2002)
In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use...
The meaning of types – from intrinsic to extrinsic semantics (2000)
John C. Reynolds, John C. Reynolds, John C. Reynolds
Copyright c
Intuitionistic reasoning about shared mutable data structure (2000)
by Palgrave. It supercedes the version (dated August 12, 1999) that was
Developing theories of types and computability via realizability (2000)
Lars Birkedal, Stephen Brookes, John C. Reynolds
We investigate the development of theories of types and computability via realizability. In the rst part of the thesis, we suggest a general notion of realizability, based on weakly closed partial...
Definitional interpreters revisited (1998)
John C. Reynolds, In Late, Jean Sammet, Burt Leavenworth, Art Evans
Abstract. To introduce the republication of “Definitional Interpreters for Higher-Order Programming Languages”, the author recounts the circumstances of its creation, clarifies several...
Design of the Programming Language Forsythe, (1997)
This is a description of the programming language Forsythe, which is a descendant of Algol 60 intended to be as uniform and general as possible, while retaining the basic character of its progenitor.
From Algol to Polymorphic Linear Lambda-calculus (1997)
Peter W. O'Hearn, Queen Mary, John C. Reynolds
ion and Store Shapes . . . . . . . . . . 6 2 Two Variations on Algol 8 2.1 Idealized Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Name: P.W. O'Hearn Address: Department of...
Design of the Programming Language Forsythe (1996)
This is a description of the programming language Forsythe, which is a descendant of Algol 60 intended to be as uniform and general as possible, while retaining the basic character of its progenitor....
From Algol to Polymorphic Linear Lambda-calculus (1996)
Peter W. O'Hearn, John C. Reynolds
We translate two variations on Algol 60 into the polymorphic linear lambda-calculus, extended with a fixed-point operator. One of the translations is for a version of Idealized Algol with side...
Solving recursive domain equations with enriched categories (1994)
Kim Ritter Wagner, Stephen Brookes, John C. Reynolds
Both pre-orders and metric spaces have been used at various times as a foundation for the solution of recursive domain equations in the area of denotational semantics. In both cases the central...
An Introduction to Polymorphic Lambda Calculus (1994)
Introduction to the Polymorphic Lambda Calculus John C. Reynolds Carnegie Mellon University December 23, 1994 The polymorphic (or second-order) typed lambda calculus was invented by Jean-Yves Girard...
The Discoveries of Continuations (1993)
John C. Reynolds, A. Van Wijngaarden, A. W. Mazurkiewicz, F. L. Morris, C. P. Wadsworth, J. H. Morris, ...
. We give a brief account of the discoveries of continuations and related concepts by A. van Wijngaarden, A. W. Mazurkiewicz, F. L. Morris, C. P. Wadsworth, J. H. Morris, M. J. Fischer, and S. K....
Types, Abstraction, and Parametric Polymorphism, Part 2 (1991)
D. A. Schmidt, Qingming Ma, John C. Reynolds
The concept of relations over sets is generalized to relations over an arbitrary category, and used to investigate the abstraction (or logical-relations) theorem, the identity extension lemma, and...
John C. Reynolds, Gordon D. Plotkin
Given a model of the polymorphic typed lambda calculus based upon a Cartesian closed category K, there will be functors from K to K whose action on objects can be expressed by type expressions and...
On functors expressible in the polymorphic typed lambda calculus (1990)
John C. Reynolds, Gordon D. Plotkin
This is a preprint of a paper that has been submitted to Information and Computation.
Senior seminar (D.V.M.)--Cornell University, 1989.
Definitional interpreters for higher-order programming languages (1972)
Abstract. Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters that are themselves written in a programming...
43 p. :
John C. Reynolds, Copyright C, John C. Reynolds, John C. Reynolds
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...