Sciweavers

ENTCS
2006
171views more  ENTCS 2006»
13 years 11 months ago
Program Extraction From Proofs of Weak Head Normalization
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...
ENTCS
2006
138views more  ENTCS 2006»
13 years 11 months ago
Variables as Resource in Separation Logic
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...
Richard Bornat, Cristiano Calcagno, Hongseok Yang
ENTCS
2006
103views more  ENTCS 2006»
13 years 11 months ago
Static Equivalence is Harder than Knowledge
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,...
Johannes Borgström
ENTCS
2006
133views more  ENTCS 2006»
13 years 11 months ago
A Data Model for Data Integration
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...
James J. Lu
ENTCS
2006
115views more  ENTCS 2006»
13 years 11 months ago
Using ATL for Checking Models
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. ...
Jean Bézivin, Frédéric Jouaul...
ENTCS
2006
110views more  ENTCS 2006»
13 years 11 months ago
The Linear Logical Abstract Machine
ar Logical Abstract Machine Eduardo Bonelli 1 LIFIA, Fac. de Inform
Eduardo Bonelli
ENTCS
2006
122views more  ENTCS 2006»
13 years 11 months ago
Abstract Effective Models
Udi Boker, Nachum Dershowitz
ENTCS
2006
339views more  ENTCS 2006»
13 years 11 months ago
A Short Visit to the STS Hierarchy
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...
Nathalie Bertrand, Ph. Schnoebelen
ENTCS
2006
146views more  ENTCS 2006»
13 years 11 months ago
Strong Update, Disposal, and Encapsulation in Bunched Typing
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 ...
Josh Berdine, Peter W. O'Hearn
ENTCS
2006
89views more  ENTCS 2006»
13 years 11 months ago
Soft Constraints for Security
Giampaolo Bella, Stefano Bistarelli, Simon N. Fole...