A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators

DOI10.1007/978-3-540-87531-4_21zbMath1156.03315OpenAlexW1512100133MaRDI QIDQ3540185

Shin-ya Katsumata

Publication date: 20 November 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-87531-4_21

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Galois connecting call-by-value and call-by-name ⋮ Relating Computational Effects by ⊤ ⊤-Lifting

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• A characterization of lambda definability in categorical models of implicit polymorphism
• Categorical logic and type theory
• A reflection theorem for closed categories
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Categories and Computer Science
• Introduction to distributive categories
• Proofs of strong normalisation for second order classical natural deduction
• Parametric polymorphism and operational equivalence
• Computer Science Logic
• Programming Languages and Systems
• Typed Lambda Calculi and Applications

This page was built for publication: A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators