Gödel's system T revisited

DOI10.1016/J.TCS.2009.11.014MaRDI QIDQ960861zbMATH OpenOpenAlexFDO

Authors Sandra Alves, Maribel Fernández, 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)

Recommendations

• The Power of Linear Functions
• Linearity and iterator types for Gödel's system \(\mathcal T\)
• The power of closed reduction strategies
• Iterator Types
• Minimality in a linear calculus with iteration

Cites work

• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 4099289 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 1392281 (Why is no real title available?)
• scientific article; zbMATH DE number 1424037 (Why is no real title available?)
• An internal language for autonomous categories
• BCK-combinators and linear \(\lambda\)-terms have types
• Bounded linear logic: A modular approach to polynomial-time computability
• Closed reduction: explicit substitutions without $\alpha$ -conversion
• Combinatory reduction systems: Introduction and survey
• Combinatory weak reduction in lambda calculus
• Computational interpretations of linear logic
• Foundations of Software Science and Computation Structures
• Intuitionistic light affine logic
• Light linear logic
• Lilac: a functional programming language based on linear logic
• Linear logic
• Linear types and non-size-increasing polynomial time computation.
• On theories with a combinatorial definition of 'equivalence'
• Soft linear logic and polynomial time
• The Power of Linear Functions
• The lambda calculus, its syntax and semantics
• The power of closed reduction strategies
• Weak linearization of the lambda calculus

Cited in

(12)

• An Interaction Net Encoding of Gödel’s System  $$\mathcal {T}$$
• Natural number objects in Dialectica categories
• Non-determinism in Gödel's system \(T\)
• The power of closed reduction strategies
• Minimality in a linear calculus with iteration
• The Power of Linear Functions
• scientific article; zbMATH DE number 1223615 (Why is no real title available?)
• A geometry of interaction machine for Gödel's system T
• On the reification of semantic linearity
• Derivation lengths classification of Gödel's T extending Howard's assignment
• Iterator Types
• Linearity and iterator types for Gödel's system \(\mathcal T\)

Describes a project that uses

Uses Software

• Lilac

This page was built for publication: Gödel's system \(\mathcal T\) revisited

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