Linear sized types in the calculus of constructions

DOI10.1007/978-3-319-07151-0_11zbMATH Open1416.68046OpenAlexW49020731MaRDI QIDQ5170709FDOQ5170709

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

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

Mathematics Subject Classification ID

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

Cited In (6)

• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Semi-continuous Sized Types and Termination
• Semi-continuous Sized Types and Termination
• Bounded Linear Types in a Resource Semiring
• A type-assignment of linear erasure and duplication
• 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)