Linear dependent types and relative completeness

DOI10.2168/LMCS-8(4:11)2012MaRDI QIDQ4899111zbMATH OpenOpenAlexFDO

Authors Ugo Dal Lago, Marco Gaboardi

Publication date 7 January 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-8(4:11)2012

zbMATH Keywords

dependent typesimplicit computational complexitylinear logicrelative completenessresource consumption

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• Linear dependent types in a call-by-value scenario
• Realizability models for a linear dependent PCF
• Linear realizability and full completeness for typed lambda-calculi
• The geometry of types
• Integrating linear and dependent types

Cited in

(24)

• Generalized bounded linear logic and its categorical semantics
• Types for complexity of parallel computation in pi-calculus
• Graded modal dependent type theory
• Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
• Realizability models for a linear dependent PCF
• Linear dependent types in a call-by-value scenario
• Higher-order interpretations and program complexity
• Mitigating multi-target attacks in hash-based signatures
• Towards a formal theory of graded monads
• Integrating linear and dependent types
• The geometry of types
• Probabilistic termination by monadic affine sized typing
• I got plenty o' nuttin'
• On paths-based criteria for polynomial time complexity in proof-nets
• The dynamic geometry of interaction machine: a token-guided graph rewriter
• Relational cost analysis in a functional-imperative setting
• Combining linear logic and size types for implicit complexity
• Denotational semantics as a foundation for cost recurrence extraction for functional languages
• scientific article; zbMATH DE number 7204445 (Why is no real title available?)
• Tight typings and split bounds, fully developed
• Non-linearity as the metric completion of linearity
• Bounded Linear Types in a Resource Semiring
• Implicit computation complexity in higher-order programming languages
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)

This page was built for publication: Linear dependent types and relative completeness

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