000			01720naa a2200241 a 4500
003			AR-LpUFIB
005			20250311170417.0
008			230201s2009 xx o 000 0 eng d
024	8		_aDIF-M6516 _b6655 _zDIF005936
040			_aAR-LpUFIB _bspa _cAR-LpUFIB
100	1		_aBonelli, Eduardo
245	1	0	_aThe logic of proofs as a foundation for certifying mobile computation
300			_a1 archivo (293,4 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 Artemov'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 normalistion for a run-time system based on an abstract machine.
534			_aLogical Foundations of Computer Science : International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings. Berlín : Springer, 2009. (Lecture Notes in Computer Science ; 5407), pp. 76-91
650		4	_aCOMPUTACIÓN MÓVIL
650		4	_aLENGUAJES DE PROGRAMACIÓN
650		4	_aPROGRAMACIÓN LÓGICA
700	1		_aFeller, Federico
856	4	0	_uhttp://dx.doi.org/10.1007/978-3-540-92687-0_6
942			_cCP
999			_c55718 _d55718