On automating the extraction of programs from termination proofs
We investigate an automated program synthesis system that is based on the paradigm of programming by proofs. To automatically extract a term that computes a recursive function given by a set of equations the system must nd a formal proof of the totality of the given function. Because of the particu...
Main Authors: | Fairouz Kamareddine, François Monin, Mauricio Ayala Rincón |
---|---|
Format: | Article |
Language: | English |
Published: |
Universidad Autónoma de Bucaramanga
2003-12-01
|
Series: | Revista Colombiana de Computación |
Online Access: | https://revistas.unab.edu.co/index.php/rcc/article/view/1088 |
Similar Items
-
Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices
by: Daniel Ventura, et al.
Published: (2010-01-01) -
Termination of Narrowing: Automated Proofs and Modularity Properties
by: Iborra López, José
Published: (2013) -
Automated termination proofs using Walther recursion
by: Wu, Alexander
Published: (2007) -
Ordinal complexity of recursive programs and their termination proofs
by: Fairtlough, Matthew V. H.
Published: (1991) -
Semantics in a Frege structure
by: Kamareddine, Fairouz Dib
Published: (1988)