Sciweavers

CSL
2004
Springer
14 years 5 months ago
A Dependent Type Theory with Names and Binding
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...
Ulrich Schöpp, Ian Stark
CSL
2004
Springer
14 years 5 months ago
Set Constraints on Regular Terms
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...
Pawel Rychlikowski, Tomasz Truderung
CSL
2004
Springer
14 years 5 months ago
Moving in a Crumbling Network: The Balanced Case
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...
Philipp Rohde
CSL
2004
Springer
14 years 5 months ago
Unsound Theorem Proving
Abstract. Applications in software verification often require determining the satisfiability of first-order formulæ with respect to some background theories. During development...
Christopher Lynch
CSL
2004
Springer
14 years 5 months ago
Axioms for Delimited Continuations in the CPS Hierarchy
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 ...
Yukiyoshi Kameyama
CSL
2004
Springer
14 years 5 months ago
The Boundary Between Decidability and Undecidability for Transitive-Closure Logics
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 ...
Neil Immerman, Alexander Moshe Rabinovich, Thomas ...
CSL
2004
Springer
14 years 5 months ago
Predicate Transformers and Linear Logic: Yet Another Denotational Model
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...
Pierre Hyvernat
CSL
2004
Springer
14 years 5 months ago
Abstract Interpretation of Proofs: Classical Propositional Calculus
Interpretation of Proofs: Classical Propositional Calculus Martin Hyland DPMMS, Centre for Mathematical Sciences, University of Cambridge, England Representative abstract interpret...
Martin Hyland
CSL
2004
Springer
14 years 5 months ago
Complete Lax Logical Relations for Cryptographic Lambda-Calculi
Abstract. Security properties are profitably expressed using notions of contextual equivalence, and logical relations are a powerful proof technique to establish contextual equiva...
Jean Goubault-Larrecq, Slawomir Lasota, David Nowa...