Resourceful program synthesis from graded linear types
From MaRDI portal
Publication:2119110
DOI10.1007/978-3-030-68446-4_8OpenAlexW3110099603MaRDI QIDQ2119110
Jack Hughes, Dominic A. Orchard
Publication date: 23 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-68446-4_8
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Focusing and polarization in linear, intuitionistic, and classical logics
- Bounded linear logic: A modular approach to polynomial-time computability
- Logic programming in a fragment of intuitionistic linear logic
- Efficient resource management for linear logic proof search
- A double category theoretic analysis of graded linear exponential comonads
- Untersuchungen über das logische Schliessen. II
- Example-directed synthesis: a type-theoretic interpretation
- Linear dependent types for differential privacy
- Backtracking, interleaving, and terminating monad transformers
- Combining effects and coeffects via grading
- A Deductive Approach to Program Synthesis
- Logic Programming with Focusing Proofs in Linear Logic
- Non-idempotent intersection types for the Lambda-Calculus
- Resource-distribution via Boolean constraints
- Computer Science Logic
- Automated Deduction – CADE-20
- Parametric effect monads and semantics of effect systems
- Bounded Linear Types in a Resource Semiring
- A Core Quantitative Coeffect Calculus
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic