TPHOL
2003
IEEE
14 years 4 months ago
2003
IEEE
This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. ...
PLDI
2005
ACM
14 years 5 months ago
2005
ACM
Today’s module systems do not effectively support information hiding in the presence of shared mutable objects, causing serious problems in the development and evolution of larg...
MKM
2007
Springer
14 years 5 months ago
2007
Springer
This paper reports on ongoing work on the project of representing the Kenzo system [15] in type theory [11].
TPHOL
2007
IEEE
14 years 5 months ago
2007
IEEE
Abstract. We present a formal treatment of normalization by evaluation in type theory. The involved semantics of simply-typed λ-calculus is exactly the simply typed fragment of th...
FOSSACS
2010
Springer
14 years 6 months ago
2010
Springer
For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. T...
POPL
2010
ACM
14 years 9 months ago
2010
ACM
Most systems based on separation logic consider only restricted forms of implication or non-separating conjunction, as full support for these connectives requires a non-trivial no...
ICFP
2005
ACM
14 years 11 months ago
2005
ACM
ICFP
2005
ACM
14 years 11 months ago
2005
ACM
We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlyi...
POPL
2003
ACM
14 years 11 months ago
2003
ACM