On Completeness of Logical Relations for Monadic Types
Loading...
Date
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Description
Software security can be ensured by specifying and verifying security properties of software using formal methods with strong theoretical bases. In particular, programs can be modeled in the framework of lambda-calculi, and interesting properties can be expressed formally by contextual equivalence (a.k.a. observational equivalence). Furthermore, imperative features, which exist in most real-life software, can be nicely expressed in the so-called computational lambda-calculus. Contextual equivalence is difficult to prove directly, but we can often use logical relations as a tool to establish it in lambda-calculi. We have already defined logical relations for the computational lambda-calculus in previous work. We devote this paper to the study of their completeness w.r.t. contextual equivalence in the computational lambda-calculus.
20 pages, full version of the paper published at ASIAN'2006, with the same title
20 pages, full version of the paper published at ASIAN'2006, with the same title
Citation
Consulte el texto completo en el siguiente enlace:
https://arxiv.org/abs/cs/0612106
http://arxiv.org/abs/cs/0612106
Advances in Computer Science - ASIAN 2006, Secure Software, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Proceedings, volume 4435 of Lecture Notes in Computer Science, pages 223-230, Springer
doi:10.1007/978-3-540-77505-8_17
http://arxiv.org/abs/cs/0612106
Advances in Computer Science - ASIAN 2006, Secure Software, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Proceedings, volume 4435 of Lecture Notes in Computer Science, pages 223-230, Springer
doi:10.1007/978-3-540-77505-8_17