CSL
2004
Springer
14 years 4 months ago
2004
Springer
We consider the problem of providing formal support for working tract syntax involving variable binders. Gabbay and Pitts have shown in their work on Fraenkel-Mostowski (FM) set th...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
Set constraints are a useful formalism for verifying properties of programs. Usually, they are interpreted over the universe of finite terms. However, some logic languages allow i...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
In this paper we continue the study of ‘sabotage modal logic’ SML which was suggested by van Benthem. In this logic one describes the progression along edges of a transition gr...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
CSL
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. Applications in software verification often require determining the satisfiability of first-order formulæ with respect to some background theories. During development...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
A CPS translation is a syntactic translation of programs, which is useful for describing their operational behavior. By iterating the standard call-by-value CPS translation, Danvy ...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
To reason effectively about programs, it is important to have some version of a transitive-closure operator so that we can describe such notions as the set of nodes reachable from ...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
In the refinement calculus, monotonic predicate transformers are used to model specifications for (imperative) programs. Together with a natural notion of simulation, they form a...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
Interpretation of Proofs: Classical Propositional Calculus Martin Hyland DPMMS, Centre for Mathematical Sciences, University of Cambridge, England Representative abstract interpret...
CSL
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. Security properties are profitably expressed using notions of contextual equivalence, and logical relations are a powerful proof technique to establish contextual equiva...