Sciweavers

Share
IFIP
2010
Springer
8 years 5 months ago
Secrecy and Authenticity Types for Secure Distributed Messaging
Abstract. We introduce a calculus with mobile names, distributed principals and primitives for secure remote communication, without any reference to explicit cryptography. The calc...
Michele Bugliesi, Stefano Calzavara, Damiano Maced...
CORR
2011
Springer
150views Education» more  CORR 2011»
8 years 5 months ago
Program Optimization Based Pointer Analysis and Live Stack-Heap Analysis
In this paper, we present type systems for flow-sensitive pointer analysis, live stack-heap (variables) analysis, and program optimization. The type system for live stack-heap ana...
Mohamed A. El-Zawawy
TACAS
2010
Springer
151views Algorithms» more  TACAS 2010»
8 years 8 months ago
A Polymorphic Intermediate Verification Language: Design and Logical Encoding
Abstract. Intermediate languages are a paradigm to separate concerns in software verification systems when bridging the gap between programming languages and the logics understood ...
K. Rustan M. Leino, Philipp Rümmer
WOLLIC
2010
Springer
8 years 8 months ago
Intersection Type Systems and Explicit Substitutions Calculi
Abstract. The λ-calculus with de Bruijn indices, called λdB, assembles each α-class of λ-terms into a unique term, using indices instead of variable names. Intersection types p...
Daniel Lima Ventura, Mauricio Ayala-Rincón,...
TOPLAS
2010
115views more  TOPLAS 2010»
8 years 8 months ago
JavaCOP: Declarative pluggable types for java
program constraints are defined over a program’s abstract syntax tree. The JAVACOP compiler automatically enforces these constraints on programs during compilation. The JAVACOP ...
Shane Markstrum, Daniel Marino, Matthew Esquivel, ...
OOPSLA
2010
Springer
8 years 8 months ago
A time-aware type system for data-race protection and guaranteed initialization
We introduce a type system based on intervals, objects representing the time in which a block of code will execute. The type system can verify time-based properties such as when a...
Nicholas D. Matsakis, Thomas R. Gross
SCP
2002
119views more  SCP 2002»
8 years 9 months ago
Polymorphic subtyping in O'Haskell
O'Haskell is a programming language derived from Haskell by the addition of concurrent reactive objects and subtyping. Because Haskell already encompasses an advanced type sy...
Johan Nordlander
LOBJET
2000
84views more  LOBJET 2000»
8 years 10 months ago
Typing Concurrent Objects and Actors
ABSTRACT. As informal methods do little to help their use for concurrent and distributed programming, one of the most challenging current tasks is to build tools based on formal me...
Fabien Dagnat, Marc Pantel, Matthias Colin, Patric...
ENTCS
2002
134views more  ENTCS 2002»
8 years 10 months ago
Implementing Compositional Analysis Using Intersection Types With Expansion Variables
A program analysis is compositional when the analysis result for a particular program fragment is obtained solely from the results for its immediate subfragments via some composit...
Assaf J. Kfoury, Geoffrey Washburn, Joe Wells
ENTCS
2000
81views more  ENTCS 2000»
8 years 10 months ago
Secrecy, Group Creation
We lift Cardelli, Ghelli and Gordon's secrecy group creation operator [1] to a relative of the spicalculus that supports symmetric key cryptography, and show a natural extens...
Luca Cardelli, Andy Gordon, Giorgio Ghelli
books