Recursive programming with proofs
From MaRDI portal
Cites work
- 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?)
- Automatic synthesis of typed -programs on term algebras
Cited in
(19)- A semantical storage operator theorem for all types
- An ordinal measure based procedure for termination of functions
- Singleton, union and intersection types for program extraction
- System ST toward a type system for extraction and proofs of programs
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- On automating the extraction of programs from proofs using product types
- Least and greatest fixed points in intuitionistic natural deduction
- Mixed Inductive/Coinductive Types and Strong Normalization
- A user's friendly syntax to define recursive functions as typed λ-terms
- Programs from proofs using classical dependent choice
- The Recursion Scheme from the Cofree Recursive Comonad
- Machine Deduction
- Strong storage operators and data types
- Automatizing termination proofs of recursively defined functions
- The Inf function in the system \(F\)
- Two extensions of System F with (co)iteration and primitive (co)recursion principles
- A new deconstructive logic: linear logic
- Proof-search in type-theoretic languages: An introduction
- Monotone recursive types and recursive data representations in Cedille
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)
