Recursive programming with proofs
From MaRDI portal
We present some methods for programming with recursive data types using a fixed-point combinator, which allows one to construct programs having their intended behaviour.
Cites work
- Automatic synthesis of typed -programs on term algebras
- scientific article; zbMATH DE number 4147469 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 1354162 (Why is no real title available?)
- scientific article; zbMATH DE number 3342819 (Why is no real title available?)
Cited in
(20)- Automatizing termination proofs of recursively defined functions
- The Inf function in the system \(F\)
- A semantical storage operator theorem for all types
- System ST toward a type system for extraction and proofs of programs
- Proof-search in type-theoretic languages: An introduction
- Strong storage operators and data types
- Programs from proofs using classical dependent choice
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- Mixed Inductive/Coinductive Types and Strong Normalization
- Two extensions of System F with (co)iteration and primitive (co)recursion principles
- A new deconstructive logic: linear logic
- On automating the extraction of programs from proofs using product types
- Monotone recursive types and recursive data representations in Cedille
- Singleton, union and intersection types for program extraction
- The Recursion Scheme from the Cofree Recursive Comonad
- An ordinal measure based procedure for termination of functions
- Least and greatest fixed points in intuitionistic natural deduction
- A user's friendly syntax to define recursive functions as typed λ-terms
- Machine Deduction
- Recursive subtyping for all
This page was built for publication: Recursive programming with proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1190480)
