Linear sized types in the calculus of constructions

DOI10.1007/978-3-319-07151-0_11MaRDI QIDQ5170709zbMATH OpenOpenAlexFDO

Authors Jorge Luis Sacchini

Publication date 24 July 2014

Published in Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-07151-0_11

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Semi-continuous Sized Types and Termination
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Linear types and non-size-increasing polynomial time computation.
• Semi-continuous Sized Types and Termination

Cited in

(6)

• A type-assignment of linear erasure and duplication
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Bounded Linear Types in a Resource Semiring
• Semi-continuous Sized Types and Termination
• Semi-continuous Sized Types and Termination
• Is sized typing for Coq practical?

This page was built for publication: Linear sized types in the calculus of constructions

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