Dependent types for program termination verification
From MaRDI portal
Publication:1850960
DOI10.1023/A:1019916231463zbMath1041.68059OpenAlexW2168162624MaRDI QIDQ1850960
Publication date: 15 December 2002
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1019916231463
Related Items (11)
Size-based termination of higher-order rewriting ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Well-founded recursion with copatterns and sized types ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ The Computability Path Ordering: The End of a Quest ⋮ Type-Based Termination with Sized Products ⋮ Termination checking with types ⋮ A Tutorial on Type-Based Termination ⋮ On the Relation between Sized-Types Based Termination and Semantic Labelling ⋮ Adapting functional programs to higher order logic ⋮ Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
Uses Software
This page was built for publication: Dependent types for program termination verification
