Justification Logic as a foundation for certifying mobile computation

We explore an intuitionistic fragment of Artëmov's Justification Logic as a type system for a programming language for mobile units. Such units consist of both a code and a certificate component. Our language, the Certifying Mobile Calculus, caters for code and certificate development in a unif...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Bonelli, Eduardo, Feller, Federico
Formato: Articulo
Lenguaje:Inglés
Publicado: 2012
Materias:
Ciencias Informáticas
Curry-de Bruijn-Howard isomorphism
Justification Logic
Mobile computation
Typed lambda calculus
Lógica
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/84399
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-84399
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Curry-de Bruijn-Howard isomorphism
Justification Logic
Mobile computation
Typed lambda calculus
Lógica
spellingShingle Ciencias Informáticas
Curry-de Bruijn-Howard isomorphism
Justification Logic
Mobile computation
Typed lambda calculus
Lógica
Bonelli, Eduardo
Feller, Federico
Justification Logic as a foundation for certifying mobile computation
topic_facet Ciencias Informáticas
Curry-de Bruijn-Howard isomorphism
Justification Logic
Mobile computation
Typed lambda calculus
Lógica
description We explore an intuitionistic fragment of Artëmov's Justification Logic as a type system for a programming language for mobile units. Such units consist of both a code and a certificate component. Our language, the Certifying Mobile Calculus, caters for code and certificate development in a unified theory. In the same way that mobile code is constructed out of code components and extant type systems track local resource usage to ensure the mobile nature of these components, our system additionally ensures correct certificate construction out of certificate components. We present proofs of type safety and strong normalization for a run-time system based on an abstract machine.
format Articulo
Articulo
author Bonelli, Eduardo
Feller, Federico
author_facet Bonelli, Eduardo
Feller, Federico
author_sort Bonelli, Eduardo
title Justification Logic as a foundation for certifying mobile computation
title_short Justification Logic as a foundation for certifying mobile computation
title_full Justification Logic as a foundation for certifying mobile computation
title_fullStr Justification Logic as a foundation for certifying mobile computation
title_full_unstemmed Justification Logic as a foundation for certifying mobile computation
title_sort justification logic as a foundation for certifying mobile computation
publishDate 2012
url http://sedici.unlp.edu.ar/handle/10915/84399
work_keys_str_mv AT bonellieduardo justificationlogicasafoundationforcertifyingmobilecomputation
AT fellerfederico justificationlogicasafoundationforcertifyingmobilecomputation
bdutipo_str Repositorios
_version_ 1764820488682471426

Ejemplares similares