Decalf equips types with an intrinsic preorder so that cost bounds for effectful programs become ordinary programs, extending Calf to probabilistic choice and other effects, with a model in augmented simplicial sets.
In Search of Effectful Dependent Types
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
abstract
Real world programming languages crucially depend on the availability of computational effects to achieve programming convenience and expressive power as well as program efficiency. Logical frameworks rely on predicates, or dependent types, to express detailed logical properties about entities. According to the Curry-Howard correspondence, programming languages and logical frameworks should be very closely related. However, a language that has both good support for real programming and serious proving is still missing from the programming languages zoo. We believe this is due to a fundamental lack of understanding of how dependent types should interact with computational effects. In this thesis, we make a contribution towards such an understanding, with a focus on semantic methods.
fields
cs.PL 2verdicts
UNVERDICTED 2representative citing papers
CHAD is a homomorphic source-to-source transformation for forward- and reverse-mode AD on higher-order functional languages with arrays, proven correct via compositional logical relations.
citing papers explorer
-
Decalf: A Directed, Effectful Cost-Aware Logical Framework
Decalf equips types with an intrinsic preorder so that cost bounds for effectful programs become ordinary programs, extending Calf to probabilistic choice and other effects, with a model in augmented simplicial sets.
-
CHAD: Combinatory Homomorphic Automatic Differentiation
CHAD is a homomorphic source-to-source transformation for forward- and reverse-mode AD on higher-order functional languages with arrays, proven correct via compositional logical relations.