A dependent dependency calculus

DOI10.1007/978-3-030-99336-8_15MaRDI QIDQ6166797zbMATH OpenOpenAlexFDO

Authors Pritam Choudhury, Harley III Eades, Stephanie Weirich

Publication date 3 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2201.11040

zbMATH Keywords

dependent typesinformation flowirrelevance

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to language design: its results can help users and compilers enforce security constraints, eliminate dead code, among other applications. In this work, we present a Dependent Dependency Calculus (DDC), which extends this general idea to the setting of a dependently-typed language. We use this calculus to track both run-time and compile-time irrelevance, enabling faster type-checking and program execution.

Recommendations

• scientific article; zbMATH DE number 2087549
• KI 2005: Advances in Artificial Intelligence
• Programming Languages and Systems
• The calculus of dependent lambda eliminations
• A classical sequent calculus with dependent types
• scientific article; zbMATH DE number 3984620
• Propositional logics of dependence
• Computing Dependencies Using FCA
• Syntactic calculus with dependent types
• Expressivity and Complexity of Dependence Logic

Cites work

• A core quantitative coeffect calculus
• A lattice model of secure information flow
• Bounded Linear Types in a Resource Semiring
• Coeffects: a calculus of context-dependent computation
• Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory
• Dependent information flow types
• Erasure and Polymorphism in Pure Type Systems
• Graded modal dependent type theory
• scientific article; zbMATH DE number 1722663 (Why is no real title available?)
• I got plenty o' nuttin'
• Notions of computation and monads
• On irrelevance and algorithmic equality in predicative type theory
• Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
• Syntax and semantics of quantitative type theory
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• Type-theory in color

Cited in

(3)

• Guessing singular dependencies
• scientific article; zbMATH DE number 2087549 (Why is no real title available?)
• Abstract semantic dependency

This page was built for publication: A dependent dependency calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166797)