Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic

DOI10.4230/lipics.types.2017.1zbMath1528.03242OpenAlexW2943087537MaRDI QIDQ6060672

Guillaume Allais

Publication date: 3 November 2023

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2018/10049/

zbMATH Keywords

linear logictype systembidirectional

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (4)

Relating Functional and Imperative Session Types ⋮ Graded modal dependent type theory ⋮ \( \pi\) with leftovers: a mechanisation in Agda ⋮ Resourceful program synthesis from graded linear types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Inductive families
• Efficient resource management for linear logic proof search
• Transporting functions across ornaments
• Bag Equivalence via a Proof-Relevant Membership Relation
• Aliasing Restrictions of C11 Formalized in Coq
• I Got Plenty o’ Nuttin’
• Dependently Typed Programming in Agda
• de Bruijn notation as a nested datatype
• A Type Theory for Probabilistic and Bayesian Reasoning
• Typed Tagless Final Interpreters
• Categorical reconstruction of a reduction free normalization proof
• System FC with explicit kind equality
• QWIRE: a core language for quantum circuits
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Types for Proofs and Programs

This page was built for publication: Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic