PLDI
2012
ACM
12 years 2 months ago
2012
ACM
JavaScript performance is often bound by its dynamically typed nature. Compilers do not have access to static type information, making generation of efficient, type-specialized m...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
Gradual typing lets programmers evolve their dynamically typed programs by gradually adding explicit type annotations, which confer benefits like improved performance and fewer r...
CORR
2012
Springer
12 years 8 months ago
2012
Springer
The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm ...
JCSS
2002
14 years 3 days ago
2002
A database programming language is a programming language extended with database operations. In this paper we extend a core functional language with explicitly labeled tuples and ...
BIRTHDAY
2005
Springer
14 years 2 months ago
2005
Springer
Abstract. We introduce an ambient-based calculus that combines ambient mobility with process mobility, uses group names to collect ambients with homologous features, and exploits c...
APLAS
2008
ACM
14 years 2 months ago
2008
ACM
This paper introduces a new type system designed for safe systems programming. The type system features a new mutability model that combines unboxed types with a consistent typing ...
CONCUR
2006
Springer
14 years 4 months ago
2006
Springer
We extend a previous type system for the -calculus that guarantees deadlock-freedom. The previous type systems for deadlockfreedom either lacked a reasonable type inference algorit...
APLAS
2004
ACM
14 years 4 months ago
2004
ACM
This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher-order programs. The ...
APLAS
2007
ACM
14 years 4 months ago
2007
ACM
Gordon and Jeffrey developed a type system for checking correspondence assertions. The correspondence assertions, proposed by Woo and Lam, state that when a certain event (called a...
ECOOP
1993
Springer
14 years 4 months ago
1993
Springer
Abstract. We have designed and implemented a type inference algorithm for the Self language. The algorithm can guarantee the safety and disambiguity of message sends, and provide u...