A deep quantitative type system

DOI10.4230/LIPICS.CSL.2021.24MaRDI QIDQ6839812zbMATH OpenFDO

Authors Giulio Guerrieri, Willem Heijltjes

Publication date 23 March 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2021.24

zbMATH Keywords

deep inferenceintersection typeslambda-calculusresource calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A filter lambda model and the completeness of type assignment
• A linearization of the Lambda-calculus and consequences
• A Local System for Classical Logic
• A Local System for Intuitionistic Logic
• A new type assignment for λ-terms
• A proof calculus which reduces syntactic bureaucracy
• A System of Interaction and Structure II: The Need for Deep Inference
• An abstract factorization theorem for explicit substitutions
• An Algorithmic Interpretation of a Deep Inference System
• An extension of basic functionality theory for -calculus
• Atomic lambda calculus: a typed lambda-calculus with explicit sharing
• Decomposing probabilistic lambda calculi
• Essential and relational models
• Execution time of λ-terms via denotational semantics and intersection types
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• scientific article; zbMATH DE number 1479634 (Why is no real title available?)
• Intersection types from a proof-theoretic perspective
• Light linear logic
• Non-idempotent intersection types for the lambda-calculus
• Non-idempotent intersection types in logical form
• On phase semantics and denotational semantics: The exponentials
• Preservation of strong normalisation modulo permutations for the structural -calculus
• Proof Complexity of the Cut-free Calculus of Structures
• Quantitative semantics of the lambda calculus. Some generalisations of the relational model
• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• Resource operators for \(\lambda\)-calculus
• Spinal atomic \(\lambda\)-calculus
• Subatomic proof systems: splittable systems
• The differential lambda-calculus
• The relational model is injective for multiplicative exponential linear logic
• The structural \(\lambda \)-calculus
• Tight typings and split bounds, fully developed
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Unsound inferences make proofs shorter
• Weighted relational models of typed lambda-calculi

This page was built for publication: A deep quantitative type system

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