Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = 'm8ha98477jv4i0is6h2nch1sd5' in /var/www/church/includes/database.mysql.inc on line 121
Proofs, Denotational Semantics and Observational Equivalences in Multiplicative Linear Logic | Gruppo di Logica e Geometria della Cognizione

Proofs, Denotational Semantics and Observational Equivalences in Multiplicative Linear Logic

2006

Michele Pagani

To appear in: Mathematical Structures in Computer Science

Abstract

We study full completeness and syntactical separability of M LL proof nets with the mix rule. The general method we use consists first in addressing the two questions in the less restrictive framework of proof structures, and then in adapting the results to proof nets.
At the level of proof structures, we find a semantical characterization of their interpretations in relational semantics, and we define an observational equivalence which is proved to be the equivalence induced by cut elimination. Hence, we obtain a semantical characterization (in coherent spaces) and an observational equivalence for the proof nets with the mix rule.

Download: sepMLL.pdf | sepMLL.ps

BibTeX


Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = 'm8ha98477jv4i0is6h2nch1sd5' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node/129', '', '216.73.216.127', 1753902660) in /var/www/church/includes/database.mysql.inc on line 121