Is sized typing for Coq practical?
From MaRDI portal
Publication:6099202
DOI10.1017/s0956796822000120arXiv1912.05601OpenAlexW4317906537MaRDI QIDQ6099202
Yu-Feng Li, William J. Bowman, Jonathan Cheung-Wai Chan
Publication date: 19 June 2023
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1912.05601
Related Items (1)
Cites Work
- Constructive proofs of the range property in lambda calculus
- A simplified proof of the Church-Rosser theorem
- On a routing problem
- Type-Based Termination with Sized Products
- Type-based termination of recursive definitions
- On Strong Normalization of the Calculus of Constructions with Type-Based Termination
- Linear Sized Types in the Calculus of Constructions
- Type-Based Productivity of Stream Definitions in the Calculus of Constructions
- Well-founded recursion with copatterns and sized types
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
- Automata, Languages and Programming
- Typed Lambda Calculi and Applications
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Is sized typing for Coq practical?
