ENTCS 2006 | Sciweavers

14

ENTCS
2006

171views more ENTCS 2006»

Program Extraction From Proofs of Weak Head Normalization

13 years 4 months ago

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...

claim paper

Read More »

16

click to vote

ENTCS
2006

138views more ENTCS 2006»

Variables as Resource in Separation Logic

13 years 4 months ago

Download www.eis.mdx.ac.uk

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

claim paper

Read More »

14

click to vote

ENTCS
2006

103views more ENTCS 2006»

Static Equivalence is Harder than Knowledge

13 years 4 months ago

Download lamp.epfl.ch

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

claim paper

Read More »

7

click to vote

ENTCS
2006

133views more ENTCS 2006»

A Data Model for Data Integration

13 years 4 months ago

Download www.mathcs.emory.edu

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

claim paper

Read More »

8

click to vote

ENTCS
2006

115views more ENTCS 2006»

Using ATL for Checking Models

13 years 4 months ago

Download tfs.cs.tu-berlin.de

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...

claim paper

Read More »

6

click to vote

ENTCS
2006

110views more ENTCS 2006»

The Linear Logical Abstract Machine

13 years 4 months ago

Download www.lifia.info.unlp.edu.ar

ar Logical Abstract Machine Eduardo Bonelli 1 LIFIA, Fac. de Inform

Eduardo Bonelli

claim paper

Read More »

6

click to vote

ENTCS
2006

122views more ENTCS 2006»

Abstract Effective Models

13 years 4 months ago

Download www.cs.tau.ac.il

Udi Boker, Nachum Dershowitz

claim paper

Read More »

24

click to vote

ENTCS
2006

339views more ENTCS 2006»

A Short Visit to the STS Hierarchy

13 years 4 months ago

Download www.lsv.ens-cachan.fr

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

claim paper

Read More »

9

click to vote

ENTCS
2006

146views more ENTCS 2006»

Strong Update, Disposal, and Encapsulation in Bunched Typing

13 years 4 months ago

Download research.microsoft.com

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

claim paper

Read More »

6

click to vote

ENTCS
2006

89views more ENTCS 2006»

Soft Constraints for Security

13 years 4 months ago