Type inference for light affine logic via constraints on words

DOI10.1016/J.TCS.2004.08.014zbMATH Open1071.03018OpenAlexW2155879600MaRDI QIDQ703485FDOQ703485

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

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

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)

Cites Work

• Linear logic
• Light linear logic
• Typability and type checking in System F are equivalent and undecidable
• Linear logic and elementary time
• Higher type recursion, ramification and polynomial time
• Safe recursion with higher types and BCK-algebra
• Soft linear logic and polynomial time
• Intuitionistic light affine logic
• Light affine lambda calculus and polynomial time strong normalization
• Phase semantics for light linear logic
• Light affine set theory: A naive set theory of polynomial time
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stratified coherence spaces: A denotational semantics for light linear logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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
• Title not available (Why is that?)
• Typing a core binary-field arithmetic in a light logic
• Title not available (Why is that?)
• 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)