We formalize two proofs of weak head normalization for the simply typed lambdacalculus in first-order minimal logic: one for normal-order reduction, and one for applicative-order ...
Malgorzata Biernacka, Olivier Danvy, Kristian St&o...
Separation logic [20,21,14] began life as an extended formalisation of Burstall's treatment of list-mutating programs [8]. It rapidly became clear that there was more that it...
There are two main ways of defining secrecy of cryptographic protocols. The first version checks if the adversary can learn the value of a secret parameter. In the second version,...
Data integration systems provide a uniform query interface (UQI) to multiple, autonomous data sources [4]. This paper presents the universal data model (UDM) that captures the sem...
Working with models often requires the ability to assert the compliance of a given model to a given set of constraints. Some tools are able to check OCL invariants on UML models. ...
The hierarchy of Symbolic Transition Systems, introduced by Henzinger, Majumdar and Raskin, is an elegant classification tool for some families of infinite-state operational model...
We present a bunched intermediate language for strong (type-changing) update and disposal of first-order references. In contrast to other substructural type systems, the additive ...