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: | , , |
|---|---|
| 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 |