자료유형  

 학위논문

Control Number  

0016934296

International Standard Book Number  

9798380384964

Dewey Decimal Classification Number  

004

Main Entry-Personal Name  

Silver, Lucas.

Publication, Distribution, etc. (Imprint  

[S.l.] : University of Pennsylvania., 2023

Publication, Distribution, etc. (Imprint  

Ann Arbor : ProQuest Dissertations & Theses, 2023

Physical Description  

1 online resource(154 p.)

General Note  

Source: Dissertations Abstracts International, Volume: 85-03, Section: A.

General Note  

Advisor: Zdancewic, Stephan.

Dissertation Note  

Thesis (Ph.D.)--University of Pennsylvania, 2023.

Restrictions on Access Note  

This item must not be sold to any third party vendors.

Summary, Etc.  

요약Interaction Trees are a recently developed form of denotational semantics for effectful programs that is executable and compositional. This dissertation uses Interaction Trees to develop reusable, language-independent tools for different classes of specifications. First, it demonstrates how to apply the Dijkstra monads (Swamy et al., 2013; Maillard et al., 2019) approach to Interaction Trees. Second, it demonstrates how to analyze the information flow properties of Interaction Trees, enabling security analysis for any programs with Interaction Tree denotations. Finally, it presents the Interaction Tree Specification framework, a program logic for Interaction Trees that enables efficient, syntactic automated proofs of properties of Interaction Trees.

Subject Added Entry-Topical Term  

Computer science.

Subject Added Entry-Topical Term  

Computer engineering.

Subject Added Entry-Topical Term  

Information science.

Index Term-Uncontrolled  

Formal specifications

Index Term-Uncontrolled  

Formal verification

Index Term-Uncontrolled  

Interaction Trees

Index Term-Uncontrolled  

Denotational semantics

Index Term-Uncontrolled  

Dijkstra monads

Added Entry-Corporate Name  

University of Pennsylvania Computer and Information Science

Host Item Entry  

Dissertations Abstracts International. 85-03A.

Host Item Entry  

Dissertation Abstract International

Electronic Location and Access  

로그인을 한후 보실 수 있는 자료입니다.

Control Number  

joongbu:641638