Structural recursive definitions in type theory
From MaRDI portal
Recommendations
Cited in
(28)- Adapting functional programs to higher order logic
- Recursive coalgebras from comonads
- Typed λ-calculus with recursive definitions
- Corecursion and non-divergence in session-typed processes
- Deriving structural hylomorphisms from recursive definitions
- Trace-Based Coinductive Operational Semantics for While
- scientific article; zbMATH DE number 5142784 (Why is no real title available?)
- scientific article; zbMATH DE number 3928338 (Why is no real title available?)
- scientific article; zbMATH DE number 179038 (Why is no real title available?)
- scientific article; zbMATH DE number 2003155 (Why is no real title available?)
- Size-based termination of higher-order rewriting
- Termination checking with types
- scientific article; zbMATH DE number 1863381 (Why is no real title available?)
- A Tutorial on Type-Based Termination
- Interactive programming in Agda -- objects and graphical user interfaces
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- scientific article; zbMATH DE number 5033853 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- A metalanguage for guarded iteration
- Least and greatest fixed points in intuitionistic natural deduction
- Is sized typing for Coq practical?
- Additive types in quantitative type theory
- Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
- Interpretations of recursively defined types
- Touring the MetaCoq project
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Type-based termination of generic programs
This page was built for publication: Structural recursive definitions in type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4219036)
