A type-assignment of linear erasure and duplication

DOI10.1016/j.tcs.2020.05.001zbMath1484.03128arXiv1912.12837OpenAlexW3024200455MaRDI QIDQ2193281

Luca Roversi, Gianluca Curzi

Publication date: 25 August 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

Boolean circuitsnumeralscut-elimination (cost)hereditarily finite permutationslinear \(\lambda\)-calculussecond-order multiplicative linear logictype-assignment

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40) Networks and circuits as models of computation; circuit complexity (68Q06)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• A class of reversible primitive recursive functions
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Weak typed Böhm theorem on IMLL
• BCK-combinators and linear \(\lambda\)-terms have types
• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• Linear logic and elementary time
• Soft linear logic and polynomial time
• The Power of Linear Functions
• From light logics to type assignments: a case study
• A Certified Study of a Reversible Programming Language
• Reversible simulations of elastic collisions
• FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness
• Uniform Circuits, & Boolean Proof Nets
• A Local Criterion for Polynomial-Time Stratified Computations
• Theoretical Computer Science

This page was built for publication: A type-assignment of linear erasure and duplication