On Completeness of Logical Relations for Monadic Types

Simple item page
dc.creatorLasota, Slawomir
dc.creatorNowak, David
dc.creatorZhang, Yu
dc.date2006-12-21
dc.date.accessioned2026-07-07T13:01:22Z
dc.date.available2026-07-07T13:01:22Z
dc.descriptionSoftware 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.
dc.description20 pages, full version of the paper published at ASIAN'2006, with the same title
dc.identifierhttps://arxiv.org/abs/cs/0612106
dc.identifierhttp://arxiv.org/abs/cs/0612106
dc.identifierAdvances 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
dc.identifierdoi:10.1007/978-3-540-77505-8_17
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/226129
dc.subjectLogic in Computer Science
dc.subjectProgramming Languages
dc.subjectD.3.1; F.3.1
dc.titleOn Completeness of Logical Relations for Monadic Types
dc.typetext

Files

Collections

arXiv