| 000 | 01473naa a2200217 a 4500 | ||
|---|---|---|---|
| 003 | AR-LpUFIB | ||
| 005 | 20250311170304.0 | ||
| 008 | 230201s2011 xx o 000 0 eng d | ||
| 024 | 8 |
_aDIF-M6515 _b6654 _zDIF003080 |
|
| 040 |
_aAR-LpUFIB _bspa _cAR-LpUFIB |
||
| 100 | 1 | _aBonelli, Eduardo | |
| 245 | 1 | 0 | _aJustification logic as a foundation for certifying mobile computation |
| 300 | _a1 archivo (322,0 kB) | ||
| 500 | _aFormato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática - UNLP (Colección BIPA/Biblioteca) | ||
| 520 | _aWe 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. | ||
| 534 | _aAnnals of Pure and Applied Logic, 163(7), pp. 935-950 | ||
| 650 | 4 | _aCOMPUTACIÓN MÓVIL | |
| 700 | 1 | _aFeller, Federico | |
| 856 | 4 | 0 | _uhttp://dx.doi.org/10.1016/j.apal.2011.09.007 |
| 942 | _cCP | ||
| 999 |
_c52934 _d52934 |
||