Sciweavers

TLDI
2005
ACM
102views Formal Methods» more  TLDI 2005»
14 years 4 months ago
An open and shut typecase
Two different ways of defining ad-hoc polymorphic operations commonly occur in programming languages. With the first form polymorphic operations are defined inductively on the...
Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie...
TLDI
2005
ACM
135views Formal Methods» more  TLDI 2005»
14 years 4 months ago
Types for describing coordinated data structures
Coordinated data structures are sets of (perhaps unbounded) data structures where the nodes of each structure may share types with the corresponding nodes of the other structures....
Michael F. Ringenburg, Dan Grossman
TLDI
2005
ACM
126views Formal Methods» more  TLDI 2005»
14 years 4 months ago
Type inference for atomicity
Atomicity is a fundamental correctness property in multithreaded programs. This paper presents an algorithm for verifying atomicity via type inference. The underlying type system ...
Cormac Flanagan, Stephen N. Freund, Marina Lifshin
TLDI
2005
ACM
151views Formal Methods» more  TLDI 2005»
14 years 4 months ago
Strict bidirectional type checking
Completely annotated lambda terms (such as are arrived at via the straightforward encodings of various types from System F) contain much redundant type information. Consequently, ...
Adam J. Chlipala, Leaf Petersen, Robert Harper
TLDI
2005
ACM
118views Formal Methods» more  TLDI 2005»
14 years 4 months ago
Non-interference for a JVM-like language
Gilles Barthe, Tamara Rezk