We define a core language combining computational and architectural primitives, and study how static typing may be used to ensure safety properties of component composition and dyn...
We present a typed calculus IL ("intermediate language") which supports the embedding of ML-like (strict, eager) and Haskell-like (non-strict, lazy) languages, without fa...
Ben Rudiak-Gould, Alan Mycroft, Simon L. Peyton Jo...
This paper presents a new program logic designed for facilitating automated reasoning about pointer programs. The program logic is directly inspired by previous work by O'Hea...
Abstract. The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calcul...
Abstract. We present a type system for a compile-time analysis of heapspace requirements of Java style object-oriented programs with explicit deallocation. Our system is based on a...
Language-based information-flow analysis is promising in protecting data confidentiality. Although much work has been carried out in this area, relatively little has been done for ...
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to d...
Model fields are specification-only fields that encode abstractions of the concrete state of a data structure. They allow specifications to describe the behavior of object-oriented...
We present and solve a path optimization problem on programs. Given a set of program nodes, called critical nodes, we find a shortest path through the program's control flow g...
Akash Lal, Junghee Lim, Marina Polishchuk, Ben Lib...