No Cover Image

Conference Paper/Proceeding/Abstract 193 views 5 downloads

Optimized Program Extraction for Induction and Coinduction / Ulrich, Berger

Sailing Routes in the World of Computation, Volume: 10936

Swansea University Author: Ulrich, Berger

Abstract

The paper proves soundness of an optimized realizability interpretationfor a logic supporting strictly positive induction and coinduction. Theoptimization concerns the special treatment of Harrop formulas whichyields simpler extracted programs. It is shown that wellfounded inductionis an instance of...

Full description

Published in: Sailing Routes in the World of Computation
ISBN: 978-3-319-94417-3 978-3-319-94418-0
ISSN: 0302-9743 1611-3349
Published: Kiel, Germany Springer
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa39885
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: The paper proves soundness of an optimized realizability interpretationfor a logic supporting strictly positive induction and coinduction. Theoptimization concerns the special treatment of Harrop formulas whichyields simpler extracted programs. It is shown that wellfounded inductionis an instance of strictly positive induction and from this a newcomputationally meaningful formulation of the Archimedean property forreal numbers is derived. An example of program extraction in computableanalysis shows that Archimedean induction can be used to eliminatecountable choice
College: College of Science
End Page: 80