From Process Logic to Program Logic
|
Descargar SCORM
Este recurso ha sido solicitado 1 veces (0 veces en los últimos 31 días).
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
|
| |
Ver
Detalles del recurso
|
|
|
From Process Logic to Program Logic
|
| Id. |
42134783 |
| Idioma |
inglés
|
| Titulo |
From Process Logic to Program Logic |
| Autor(es) |
Queen Mary London
|
| Localización |
http://citeseer.ist.psu.edu/699247.html
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
We present a process logic for the p-calculus with the linear/affine
type discipline [6, 7, 31, 32, 33, 59, 60]. Built on the preceding
studies on logics for programs and processes, simple systems of
assertions are developed, capturing the classes of behaviours ranging
from purely functional interactions to those with destructive
update, local state and genericity. A central feature of the logic
is representation of the behaviour of an environment as the dual
of that of a process in an assertion, which is crucial for obtaining
compositional proof systems. From the process logic we can
derive compositional program logics for various higher-order programming
languages, whose soundness is proved via their embeddings
into the process logic. In this paper, the key technical framework
of the process logic and its applications is presented focussing
on pure functional behaviour and a prototypical call-by-value functional
language, leaving the full technical development to [27, 26].
Categories and Subject Descriptors
D.3.1 [Formal Definitions and Theory]: Semantics; F.3.1 [Specifying
and Verifying and Reasoning about Programs]: Assertions, Logics
of programs, Specification techniques; F.3.2 [Semantics of Programming
Lanugages]: Process models
General Terms
Language, Theory, Verification
Keywords
Types, Mobile Processes, Higher-Order Functions, Hoare Logic,
Duality, p-Calculus
1.
|
| Tipo |
ps
|
| Palabras clave |
Queen Mary London From Process Logic to Program Logic
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
unrestricted |
| Formatos |
ps
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://www.doc.ic.ac.uk/~yoshida/paper/icfp04.ps
[References] oai:CiteSeerPSU:648256
[References] oai:CiteSeerPSU:319642
[References] oai:CiteSeerPSU:665752
[References] oai:CiteSeerPSU:624632
[References] oai:CiteSeerPSU:29355
[References] oai:CiteSeerPSU:643195
[References] oai:CiteSeerPSU:58989
[References] oai:CiteSeerPSU:191046
[References] oai:CiteSeerPSU:539315
[References] oai:CiteSeerPSU:450075
[References] oai:CiteSeerPSU:122091
[References] oai:CiteSeerPSU:196173
[References] oai:CiteSeerPSU:7751
[References] oai:CiteSeerPSU:721472
[References] oai:CiteSeerPSU:553036
[References] oai:CiteSeerPSU:460561
|
| Fecha de contribución |
31-mar-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
