The logic of proofs as a foundation for certifying mobile computation

Eduardo Bonelli, Federico Feller

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

Abstract

We explore an intuitionistic fragment of Artëmov's Logic of Proofs as a type system for a programming language for mobile units. Such units consist of both a code and certificate component. Dubbed the Certifying Mobile Calculus, our language caters for both 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
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2009, Proceedings
Pages76-91
Number of pages16
DOIs
StatePublished - 2009
EventInternational Symposium on Logical Foundations of Computer Science, LFCS 2009 - Deerfield Beach, FL, United States
Duration: 3 Jan 20096 Mar 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5407 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Symposium on Logical Foundations of Computer Science, LFCS 2009
Country/TerritoryUnited States
CityDeerfield Beach, FL
Period3/01/096/03/09

Fingerprint

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

Cite this