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 (19)

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

This page was built for publication: Recursive programming with proofs