Browsing LCS Technical Memos (1974 - 2003) by Author "Halpern, Joseph Y."
Now showing items 1-6 of 6
-
Axiomatic Definitions of Programming Languages: A Theoretical Assessment
Meyer, Albert R.; Halpern, Joseph Y. (1980-04)A precise definition is given of how partial correctness or termination assertions serve to define the semantics of classees of program schemes. Assertions involving only formulas of first order predicate calculus are ... -
Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness
Ben-Ari, Mordechai; Halpern, Joseph Y.; Pnueli, Amir (1981-01)Let p be a formular in deterministic propositional dynamic logic. A decision procedure for the satisfiability of p is given along with a construction of a finite model for every satisifiable p. The decision procedure runs ... -
From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview
Trakhtenbrot, B.A.; Halpern, Joseph Y.; Meyer, Albert R. (1983-10)The advantages of denotational over operational semantics are argued. A denotational semantics is provided for an ALGOL-like language with finite-model procedures, blocks with local storage, and sharing (aliasing). Procedure ... -
On the Expressive Power of Dynamic Logic, II
Halpern, Joseph Y. (1981-08) -
The Propositional Dynamic Logic of Deterministic, Well-Structured Programs
Halpern, Joseph Y.; Reif, John H. (1981-03)We consider a restricted propositional dynamic logic, Strict Deterministic Propositional Dynamic Logic (SDPDL), which is appropriate for reasoning about deterministic well-structured programs. In contrast to PDL, for which ... -
The Semantics of Local Storage of What Makes The Free-list Free?
Halpern, Joseph Y.; Meyer, Albert R.; Trakhtenbrot, B.A. (1984-04)Denotational semantics for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing) is given by translating programs into an appropriately typed lambda-calculus. Procedures are ...