Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
The Logic of Proofs as a Foundation for Certifying Mobile Computation
verfasst von : Eduardo Bonelli, Federico Feller
Erschienen in: Logical Foundations of Computer Science
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.