Skip navigation
  • Home
  • Browse
    • Communities
      & Collections
    • Browse Items by:
    • Publication Date
    • Author
    • Title
    • Subject
    • Department
  • Sign on to:
    • My MacSphere
    • Receive email
      updates
    • Edit Profile


McMaster University Home Page
  1. MacSphere
  2. Open Access Dissertations and Theses Community
  3. Open Access Dissertations and Theses
Please use this identifier to cite or link to this item: http://hdl.handle.net/11375/18923
Title: Assignment Calculus: A Pure Imperative Reasoning Language
Authors: Bender, Marc
Advisor: Zucker, Jeffery
Department: Computer Science
Keywords: calculus, language, reasoning, imperative, procedure, composition
Publication Date: 23-Aug-2010
Abstract: <p> In this thesis, we undertake a study of imperative reasoning. Beginning with a philosophical analysis of the distinction between imperative and functional language features, we define a (pure) imperative language as one whose constructs are inherently referentially opaque. We then give a definition of a reasoning language by identifying desirable properties such a language should have.</p> <p> The rest of the thesis presents a new pure imperative reasoning language, Assignment Calculus AC. The main idea behind AC is that R. Montague's modal operators of intension and extension are useful tools for modeling procedures in programming languages. This line of thought builds on T. Janssen's demonstration that Montague's intensional logic is well suited to dealing with assignment statements, pointers, and other difficult features of imperative languages.</p> <p> AC consists of only four basic constructs, assignment 'X := t', sequence 't; u', procedure formation 'it' and procedure invocation '!t'. Three interpretations are given for AC: an operational semantics, a denotational semantics, and a term-rewriting system. The three are shown to be equivalent. Running examples are used to illustrate each of the interpretations.</p> <p> Five variants of AC are then studied. By removing restrictions from AC's syntactic and denotational definitions, we can incorporate L-values, lazy evaluation, state backtracking, and procedure composition into AC. By incorporating procedure composition, we show that AC becomes a self-contained Turing complete language in the same way as the untyped λ-calculus: by encoding numerals, Booleans, and control structures as AC terms. Finally we look at the combination of AC with a typed λ-calculus.</p>
URI: http://hdl.handle.net/11375/18923
Appears in Collections:Open Access Dissertations and Theses

Files in This Item:
File Description SizeFormat 
Bender_Marc_2010Aug_Ph.D..pdf
Open Access
3.99 MBAdobe PDFView/Open
Show full item record Statistics


Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.

Sherman Centre for Digital Scholarship     McMaster University Libraries
©2022 McMaster University, 1280 Main Street West, Hamilton, Ontario L8S 4L8 | 905-525-9140 | Contact Us | Terms of Use & Privacy Policy | Feedback

Report Accessibility Issue