Type inference for light affine logic via constraints on words

DOI10.1016/J.TCS.2004.08.014MaRDI QIDQ703485zbMATH OpenOpenAlexFDO

Authors Patrick Baillot

Publication date 11 January 2005

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

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

zbMATH Keywords

Linear logicConstraintsImplicit computational complexityLambda-calculusLight affine logicPolynomial time complexityType inference

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 2061704
• Typed Lambda Calculi and Applications
• From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing
• scientific article; zbMATH DE number 2182488
• Type Inference for a Polynomial Lambda Calculus

Cites work

• scientific article; zbMATH DE number 1670494 (Why is no real title available?)
• scientific article; zbMATH DE number 1722649 (Why is no real title available?)
• scientific article; zbMATH DE number 445159 (Why is no real title available?)
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• scientific article; zbMATH DE number 2061704 (Why is no real title available?)
• scientific article; zbMATH DE number 2061714 (Why is no real title available?)
• scientific article; zbMATH DE number 1392281 (Why is no real title available?)
• scientific article; zbMATH DE number 1424054 (Why is no real title available?)
• Higher type recursion, ramification and polynomial time
• Intuitionistic light affine logic
• Light affine lambda calculus and polynomial time strong normalization
• Light affine set theory: A naive set theory of polynomial time
• Light linear logic
• Linear logic
• Linear logic and elementary time
• Phase semantics for light linear logic
• Safe recursion with higher types and BCK-algebra
• Soft linear logic and polynomial time
• Stratified coherence spaces: A denotational semantics for light linear logic
• Typability and type checking in System F are equivalent and undecidable

Cited in

(13)

• Theoretical Computer Science
• Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
• From ML to ML ^F
• Light types for polynomial time computation in lambda calculus
• scientific article; zbMATH DE number 2061704 (Why is no real title available?)
• Typing a core binary-field arithmetic in a light logic
• scientific article; zbMATH DE number 2182488 (Why is no real title available?)
• Optimizing optimal reduction
• Typed Lambda Calculi and Applications
• Light affine logic as a programming language: a first contribution
• Controlling Program Extraction in Light Logics
• Type Inference for a Polynomial Lambda Calculus
• Polynomial time over the reals with parsimony

This page was built for publication: Type inference for light affine logic via constraints on words

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