Recursive programming with proofs
From MaRDI portal
Publication:1190480
DOI10.1016/0304-3975(92)90042-EzbMath0759.68014MaRDI QIDQ1190480
Publication date: 26 September 1992
Published in: Theoretical Computer Science (Search for Journal in Brave)
Related Items
Automatizing termination proofs of recursively defined functions, The Inf function in the system \(F\), Monotone recursive types and recursive data representations in Cedille, A semantical storage operator theorem for all types, Singleton, union and intersection types for program extraction, Mixed Inductive/Coinductive Types and Strong Normalization, A user's friendly syntax to define recursive functions as typed λ-terms, Machine Deduction, System ST toward a type system for extraction and proofs of programs, A new deconstructive logic: linear logic, AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS, On automating the extraction of programs from proofs using product types, The Recursion Scheme from the Cofree Recursive Comonad, Programs from proofs using classical dependent choice, An ordinal measure based procedure for termination of functions, Least and greatest fixed points in intuitionistic natural deduction, Strong storage operators and data types, Two extensions of system F with (co)iteration and primitive (co)recursion principles, Proof-search in type-theoretic languages: An introduction
Uses Software
Cites Work
