東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

A low-level typed assembly language ...

Chen, Juan.

Linked to FindBook

Google Book

Amazon

博客來

A low-level typed assembly language with a machine-checkable soundness proof.

Record Type:	Electronic resources : Monograph/item
Title/Author:	A low-level typed assembly language with a machine-checkable soundness proof./
Author:	Chen, Juan.
Description:	175 p.
Notes:	Source: Dissertation Abstracts International, Volume: 65-01, Section: B, page: 0283.
Contained By:	Dissertation Abstracts International65-01B.
Subject:	Computer Science. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3119377
ISBN:	0496667731

A low-level typed assembly language with a machine-checkable soundness proof.
Chen, Juan.

A low-level typed assembly language with a machine-checkable soundness proof. - 175 p.

Source: Dissertation Abstracts International, Volume: 65-01, Section: B, page: 0283.

Thesis (Ph.D.)--Princeton University, 2004.

To verify the safety of a machine-language program, the Proof-Carrying Code framework requires machine code accompanied by a proof of safety. Typed assembly languages provide a way to generate such safety proofs automatically. But the soundness proofs of most existing typed assembly languages are hand-written and cannot be machine-checked, which is worrisome for such large calculi.

ISBN: 0496667731Subjects--Topical Terms:

626642
Computer Science.

A low-level typed assembly language with a machine-checkable soundness proof.
LDR:02186nmm 2200289 4500 001 1841060
005 20050823122906.5
008 130614s2004 eng d
020 $a 0496667731
035 $a (UnM)AAI3119377
035 $a AAI3119377
040 $a UnM $c UnM
100 1 $a Chen, Juan. $3 1917453
245 1 2 $a A low-level typed assembly language with a machine-checkable soundness proof.
300 $a 175 p.
500 $a Source: Dissertation Abstracts International, Volume: 65-01, Section: B, page: 0283.
500 $a Adviser: Andrew Appel.
502 $a Thesis (Ph.D.)--Princeton University, 2004.
520 $a To verify the safety of a machine-language program, the Proof-Carrying Code framework requires machine code accompanied by a proof of safety. Typed assembly languages provide a way to generate such safety proofs automatically. But the soundness proofs of most existing typed assembly languages are hand-written and cannot be machine-checked, which is worrisome for such large calculi.
520 $a In this dissertation I explain a low-level typed assembly language (LTAL) with a semantic model that proves LTAL's soundness with a machine-checkable proof. Compared to existing typed assembly languages, LTAL is more scalable and more secure; it has no macro instructions that hinder low-level optimizations such as instruction scheduling; its type constructors are expressive enough to capture dataflow information, support the compiler's choice of data representations and permit typed position-independent code; and its type-checking algorithm is completely syntax-directed.
520 $a I also explain a prototype system that uses LTAL to compile core ML to Sparc code and generate safety proofs. I show how we were able to build type-preserving back end based on an untyped one, without restricting low-level optimizations and without knowledge of a type system pervading the instruction selector and register allocator.
590 $a School code: 0181.
650 4 $a Computer Science. $3 626642
690 $a 0984
710 2 0 $a Princeton University. $3 645579
773 0 $t Dissertation Abstracts International $g 65-01B.
790 1 0 $a Appel, Andrew, $e advisor
790 $a 0181
791 $a Ph.D.
792 $a 2004
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3119377