서브메뉴
검색
Dependency and Linearity Analyses in Pure Type Systems- [electronic resource]
Dependency and Linearity Analyses in Pure Type Systems- [electronic resource]
상세정보
- 자료유형
- 학위논문
- Control Number
- 0016934183
- International Standard Book Number
- 9798380385343
- Dewey Decimal Classification Number
- 004
- Main Entry-Personal Name
- Choudhury, Pritam.
- 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(439 p.)
- General Note
- Source: Dissertations Abstracts International, Volume: 85-03, Section: B.
- General Note
- Advisor: Weirich, Stephanie.
- 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.
- 요약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
- 로그인을 한후 보실 수 있는 자료입니다.
- Control Number
- joongbu:642619
MARC
008240221s2023 ulk 00 kor■001000016934183
■00520240214101538
■006m o d
■007cr#unu||||||||
■020 ▼a9798380385343
■035 ▼a(MiAaPQ)AAI30572686
■040 ▼aMiAaPQ▼cMiAaPQ
■0820 ▼a004
■1001 ▼aChoudhury, Pritam.
■24510▼aDependency and Linearity Analyses in Pure Type Systems▼h[electronic resource]
■260 ▼a[S.l.]▼bUniversity of Pennsylvania. ▼c2023
■260 1▼aAnn Arbor▼bProQuest Dissertations & Theses▼c2023
■300 ▼a1 online resource(439 p.)
■500 ▼aSource: Dissertations Abstracts International, Volume: 85-03, Section: B.
■500 ▼aAdvisor: Weirich, Stephanie.
■5021 ▼aThesis (Ph.D.)--University of Pennsylvania, 2023.
■506 ▼aThis item must not be sold to any third party vendors.
■520 ▼aDependency 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.
■590 ▼aSchool code: 0175.
■650 4▼aComputer science.
■650 4▼aComputer engineering.
■650 4▼aInformation technology.
■653 ▼aDependent types
■653 ▼aGraded type systems
■653 ▼aDependency analysis
■653 ▼aProgramming languages
■653 ▼aPure Type Systems
■653 ▼aData security
■690 ▼a0984
■690 ▼a0489
■690 ▼a0464
■71020▼aUniversity of Pennsylvania▼bComputer and Information Science.
■7730 ▼tDissertations Abstracts International▼g85-03B.
■773 ▼tDissertation Abstract International
■790 ▼a0175
■791 ▼aPh.D.
■792 ▼a2023
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T16934183▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
■980 ▼a202402▼f2024
