Skip to main content

Universal properties of impure programming languages

Sam Staton, Paul Blain Levy

DOI 10.1145/2429069.2429091 dblp BibTeX

Abstract

We investigate impure, call-by-value programming languages. Our first language only has variables and let-binding. Its equational theory is a variant of Lambek's theory of multicategories that omits the commutativity axiom.

Related papers

Pure Versus Impure Lisp TOPLAS 1997
Pure versus Impure LISP POPL 1996
A reasonably exceptional type theory ICFP 2019
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq POPL 2023
Abstract Domains for Universal and Existential Properties ESOP 2000
FreeSpec: specifying, verifying, and executing impure computations in Coq CPP 2020
Property-Directed Inference of Universal Invariants or Proving Their Absence CAV 2015
Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq JFP 2025