A program logic for fresh name generation

Eliott, Harold Pancho Gordon (2022) A program logic for fresh name generation. Doctoral thesis (PhD), University of Sussex.

[img] PDF - Published Version
Download (1MB)

Abstract

This thesis introduces a program logic for an extension of the call-by-value simply typed λ-calculus (STLC), with a mechanism for the generation of fresh names via gensym, which is an adaptation of Pitts and Stark s ν-calculus 52 . Names can be compared for equality and inequality, producing programs with subtle observable properties.

Hidden names, produced by interactions between name generation and λ-abstraction, are captured logically with a new restricted quantification. The restrictions require only derived values from previously derived terms, ensuring hidden names are not revealed. The concept of derivation is extended to type contexts and models, ensuring hidden names are not revealed at later stages. Type contexts are adapted to include an order and the ability to represent future extensions. The logic quantifies over future extensions, using a second-order quantification over future type contexts. This quantification names the future context to allow for them to be reasoned about within the logic.

A new model construction is introduced to replicate the order in which names and values are produced with potentially hidden names. The semantics of the logic in the new model are used to prove each axiom and rule sound and as such the soundness of the logic. A proof that the logic is an extension of the STLC logic is given alongside a sketch of the proof that the extension is conservative.

Usage of the logic is illustrated through reasoning about numerous examples. These ex- amples range from simple STLC and ν-calculus examples to well-known difficult programs from the literature.

Item Type: Thesis (Doctoral)
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science > QA0076.6 Programming
T Technology > TK Electrical engineering. Electronics Nuclear engineering > TK7800 Electronics > TK7885 Computer engineering. Computer hardware
Depositing User: Library Cataloguing
Date Deposited: 04 May 2022 08:53
Last Modified: 04 May 2022 08:53
URI: http://sro.sussex.ac.uk/id/eprint/105641

View download statistics for this item

📧 Request an update