Gödel's system \(\mathcal T\) revisited

DOI10.1016/j.tcs.2009.11.014zbMath1191.68154OpenAlexW2068709824MaRDI QIDQ960861

Maribel Fernández, Sandra Alves, Mário Florido, Ian Mackie

Publication date: 29 March 2010

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2009.11.014

zbMATH Keywords

linearity\(\lambda \)-calculusclosed reductionsystem \(\mathcal T\)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Natural number objects in Dialectica categories ⋮ Linearity and iterator types for Gödel's system \(\mathcal T\) ⋮ On the reification of semantic linearity ⋮ An Interaction Net Encoding of Gödel’s System  $$\mathcal {T}$$

Uses Software

• Lilac

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Computational interpretations of linear logic
• BCK-combinators and linear \(\lambda\)-terms have types
• Combinatory weak reduction in lambda calculus
• The lambda calculus, its syntax and semantics
• Bounded linear logic: A modular approach to polynomial-time computability
• Light linear logic
• Combinatory reduction systems: Introduction and survey
• An internal language for autonomous categories
• Linear types and non-size-increasing polynomial time computation.
• Soft linear logic and polynomial time
• Weak linearization of the lambda calculus
• On theories with a combinatorial definition of 'equivalence'
• The Power of Closed Reduction Strategies
• The Power of Linear Functions
• Closed reduction: explicit substitutions without $\alpha$ -conversion
• Lilac: a functional programming language based on linear logic
• Foundations of Software Science and Computation Structures
• Intuitionistic Light Affine Logic