Justification Logic as a foundation for certifying mobile computation

Eduardo Bonelli, Federico Feller

Research output: Contribution to journalArticlepeer-review

4 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)935-950
Number of pages16
JournalAnnals of Pure and Applied Logic
Volume163
Issue number7
DOIs
StatePublished - Jul 2012

Keywords

  • Curry-de Bruijn-Howard isomorphism
  • Justification Logic
  • Mobile computation
  • Typed lambda calculus

Fingerprint

Dive into the research topics of 'Justification Logic as a foundation for certifying mobile computation'. Together they form a unique fingerprint.

Cite this