A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization

DOI10.1016/j.ic.2015.12.012zbMath1339.68039arXiv1410.6298OpenAlexW1904606068MaRDI QIDQ276268

Erika De Benedetti, Simonetta Ronchi della Rocca

Publication date: 3 May 2016

Published in: Information and Computation (Search for Journal in Brave)

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

zbMATH Keywords

polynomial timelambda-calculusimplicit computational complexitystratified typestype assignment systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items (5)

Tight typings and split bounds, fully developed ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ The bang calculus revisited ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Linear logic
• The parametric lambda calculus. A metamodel for computation.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A type assignment system for game semantics
• Light types for polynomial time computation in lambda calculus
• An extension of basic functionality theory for \(\lambda\)-calculus
• Light linear logic
• Perpetual reductions in \(\lambda\)-calculus
• Soft linear logic and polynomial time
• Principality and type inference for intersection types using expansion variables
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• The Inhabitation Problem for Non-idempotent Intersection Types
• Solvability in Resource Lambda-Calculus
• A PolyTime Functional Language from Light Linear Logic
• A Soft Type Assignment System for λ-Calculus
• Not Enough Points Is Enough
• Intersection types and λ-definability
• A linearization of the Lambda-calculus and consequences
• Execution time of λ-terms via denotational semantics and intersection types
• ML with PTIME complexity guarantees
• The emptiness problem for intersection types
• Essential and relational models
• Intuitionistic Light Affine Logic

This page was built for publication: A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization