Recursive programming with proofs

DOI10.1016/0304-3975(92)90042-EzbMath0759.68014MaRDI QIDQ1190480

Michel Parigot

Publication date: 26 September 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

fixed-point combinatorprogramming with recursive data typesrecursive type theory

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

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

• Nuprl

Cites Work

• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item