Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

13

LFCS
2009
Springer

favoriteEmaildiscussreport

223views Artificial Intelligence» more LFCS 2009»

The Logic of Proofs as a Foundation for Certifying Mobile Computation

13 years 11 months ago

The Logic of Proofs as a Foundation for Certifying Mobile Computation

Download www.lifia.info.unlp.edu.ar

We explore an intuitionistic fragment of Art¨emov’s Logic of Proofs as a type system for a programming language for mobile units. Such units consist of both a code and certiﬁcate component. Dubbed the Certifying Mobile Calculus, our language caters for both code and certiﬁcate development in a uniﬁed 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 certiﬁcate construction out of certiﬁcate components. We present proofs of type safety and strong normalization n-time system based on an abstract machine.

Eduardo Bonelli, Federico Feller

Real-time Traffic

Artificial Intelligence | Certiﬁcate Components | Code | LFCS 2009 | Mobile Units |

claim paper

Related Content

» Certified software

» Foundational Certified Code in a Metalogical Framework

» Asserting Bytecode Safety

» Certifying Solutions to Permutation Group Problems

» Proving Bounds on RealValued Functions with Computations

» Modular Certification of LowLevel Intermediate Representation Programs

» An expressive scalable type theory for certified code

» Beluga Programming with Dependent Types Contextual Data and Contexts

» Using XCAP to Certify Realistic Systems Code Machine Context Management

Post Info
More Details (n/a)

Added	27 May 2010
Updated	27 May 2010
Type	Conference
Year	2009
Where	LFCS
Authors	Eduardo Bonelli, Federico Feller

Comments (0)