An Operational Logic of Effects
|
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
|
|
|
An Operational Logic of Effects
|
| Id. |
46632260 |
| Idioma |
inglés
|
| Titulo |
An Operational Logic of Effects |
| Autor(es) |
Jacob Frost
Ian A. Mason
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.5539
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
In this paper we describe our progress towards an operational implementation of a modern programming logic. The logic is inspired by the variable type systems of Feferman, and is designed for reasoning about imperative functional programs. The logic goes well beyond traditional programming logics, such as Hoare's logic and Dynamic logic in its expressibility, yet is less problematic to encode into higher-order logics. The main focus of the paper is too present an axiomatization of the base first-order theory, and an implementation of the logic into the generic proof assistant Isabelle. We also indicate the directions of our current research to blend these two advances into an operational whole. Keywords semantics, logic, derivation, verification, specification, theorem proving. 1 Introduction In this paper we continue the investigations into a Variable Typed Logic of Effects that began in [20, 11, 21, 23, 12]. In particular we present an axiomatization of the base first-order theory...
|
| Tipo |
application/postscript
|
| Palabras clave |
logic
|
| Tipo de recurso |
Texto Narrativo
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| Formatos |
application/postscript
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://turing.une.edu.au/~iam/Data/Papers/96cats.ps
[References] 10.1.1.12.8714
[References] 10.1.1.26.2787
[References] 10.1.1.35.3542
[References] 10.1.1.47.9447
[References] 10.1.1.32.3754
[References] 10.1.1.50.9403
[References] 10.1.1.52.6098
[References] 10.1.1.50.3657
[References] 10.1.1.56.1123
[References] 10.1.1.48.9966
[References] 10.1.1.52.2686
[References] 10.1.1.52.3265
[References] 10.1.1.55.8516
[References] 10.1.1.16.4061
[References] 10.1.1.48.4648
[References] 10.1.1.83.2371
[References] 10.1.1.51.5027
|
| Fecha de contribución |
31-jul-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
