Material Type  

 학위논문

 

0016934183

Date and Time of Latest Transaction  

20240214101538

ISBN  

9798380385343

DDC  

004

Author  

Choudhury, Pritam.

Title/Author  

Dependency and Linearity Analyses in Pure Type Systems - [electronic resource]

Publish Info  

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

Publish Info  

Ann Arbor : ProQuest Dissertations & Theses, 2023

Material Info  

1 online resource(439 p.)

General Note  

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

General Note  

Advisor: Weirich, Stephanie.

학위논문주기  

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

Restrictions on Access Note  

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

Abstracts/Etc  

요약Dependency analysis is necessary to ensure proper flow of information in programming languages. Linearity analysis is necessary to ensure proper usage of resources in programming languages. These analyses are used for many purposes: for example, analyzing binding-time for partial evaluation of programs, ensuring data security in programs, ensuring deadlock freedom in concurrent programs, etc. What connects these analyses is that both of them need to model at least two different worlds with constrained mutual interaction. To elaborate, a typical dependency analysis may model low-security and high-security worlds with the constraint that information never leaks from the high-security world to the low-security world; a typical linearity analysis may model nonlinear and linear worlds with the constraint that derivations in the nonlinear world cannot make use of assumptions from the linear world. To statically enforce such constraints, dependency and linear type systems are employed. Several dependency and linear type systems have been proposed in literature, especially with respect to simple and polymorphic types. However, with respect to dependent types, the two analyses have not been explored much.This dissertation explores how dependent types interact with dependency and linearity analyses. More precisely, in this dissertation, we extend dependency and linearity analyses to Pure Type Systems, which include several well-known dependent type systems. We build upon existing work on graded type systems to develop three specific graded calculi for Pure Type Systems: DDC for dependency analysis, GraD for linearity analysis and LDC for combined dependency and linearity analysis. Our thesis is that these calculi provide a systematic way for analyzing dependency, linearity or a combination of the two in any Pure Type System. We study the metatheoretic properties of these calculi, show soundness of their analyses, discuss their applications and position them in the milieu of other dependency and linear calculi. Overall, our work provides insight into several nuances, hitherto unknown, of dependency and linearity analyses and their interactions with dependent types.

Subject Added Entry-Topical Term  

Computer science.

Subject Added Entry-Topical Term  

Computer engineering.

Subject Added Entry-Topical Term  

Information technology.

Index Term-Uncontrolled  

Dependent types

Index Term-Uncontrolled  

Graded type systems

Index Term-Uncontrolled  

Dependency analysis

Index Term-Uncontrolled  

Programming languages

Index Term-Uncontrolled  

Pure Type Systems

Index Term-Uncontrolled  

Data security

Added Entry-Corporate Name  

University of Pennsylvania Computer and Information Science

Host Item Entry  

Dissertations Abstracts International. 85-03B.

Host Item Entry  

Dissertation Abstract International

Electronic Location and Access  

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

소장사항  

202402 2024

Control Number  

joongbu:642619