Index-stratified types

DOI10.4230/LIPICS.FSCD.2018.19MaRDI QIDQ4993349zbMATH OpenFDO

Authors Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau

Publication date 15 June 2021

Full work available at URL https://arxiv.org/abs/1805.00401

zbMATH Keywords

(co)recursive typesindexed typeslogical relations

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 7324347
• scientific article; zbMATH DE number 2006633
• Self types for dependently typed lambda encodings
• Programming with binders and indexed data-types
• Meta-theory à la carte

Cites work

• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Combining deduction modulo and logics of fixed-point definitions
• Computer Science Logic
• Contextual modal type theory
• Cut elimination for a logic with induction and co-induction
• Guarded recursive datatype constructors
• Indexed codata types
• Intensional interpretations of functionals of finite type I
• Programming with binders and indexed data-types
• Proof normalization modulo
• Reasoning with higher-order abstract syntax in a logical framework
• Stratification in logics of definitions
• Theorem proving modulo
• Types for Proofs and Programs
• Well-founded recursion over contextual objects

Cited in

(4)

• Harpoon: mechanizing metatheory interactively
• scientific article; zbMATH DE number 2090025 (Why is no real title available?)
• POPLMark reloaded: mechanizing proofs by logical relations
• A case study in programming coinductive proofs: Howe's method

This page was built for publication: Index-stratified types

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