PACT
2001
Springer
14 years 4 months ago
2001
Springer
We introduce the νSPI-calculus that strengthens the notion of “perfect symmetric cryptography” of the spi-calculus by taking time into account. This involves defining an oper...
IFL
2001
Springer
14 years 4 months ago
2001
Springer
Abstract. J. Launchbury gave an operational semantics for lazy evaluation and showed that it is sound and complete w.r.t. a denotational s of the language. P. Sestoft then introduc...
ESMART
2001
Springer
14 years 5 months ago
2001
Springer
This paper presents an operational semantics for a subset of Java Card bytecode, focussing on aspects of the Java Card firewall, method invocation, field access, variable access,...
TPHOL
2002
IEEE
14 years 5 months ago
2002
IEEE
Abstract. This paper describes a formalization of the weakest precondition, wp, for general recursive programs using the type-theoretical proof assistant Coq. The formalization is ...
FOSSACS
2003
Springer
14 years 5 months ago
2003
Springer
We describe a metalanguage MMML, which makes explicit the order of evaluation (in the spirit of monadic metalanguages) and the staging of computations (as in languages for multi-l...
FOSSACS
2003
Springer
14 years 5 months ago
2003
Springer
We define an operational semantics and a type system for manipulating semistructured data that contains hidden information. The data model is simple labeled trees with a hiding op...
CHARME
2003
Springer
14 years 5 months ago
2003
Springer
This paper shows how classic inductive assertions can be used in conjunction with an operational semantics to prove partial correctness properties of programs. The method imposes o...
ASIAN
2003
Springer
14 years 5 months ago
2003
Springer
Abstract. The concept of unreliable failure detectors for reliable distributed systems was introduced by Chandra and Toueg as a fine-grained means to add weak forms of synchrony i...
ADC
2003
Springer
14 years 5 months ago
2003
Springer
Mathematics is forcing towards a consistent framework of theory development. Computer Science is an engineering discipline and sometimes suffers from ad-hoc definitions. Transac...
PPDP
2004
Springer
14 years 5 months ago
2004
Springer
We introduce the theoretical basis for tracing lazy functional logic computations in a declarative multi-paradigm language like Curry. Tracing computations is a difficult task due...