Program extraction from proofs: computable analysis and parser generation
25 Pages
English
Gain access to the library to view online
Learn more

Program extraction from proofs: computable analysis and parser generation

-

Gain access to the library to view online
Learn more
25 Pages
English

Description

Niveau: Supérieur
Program extraction from proofs: computable analysis and parser generation Ulrich Berger – Swansea Joint work with Monika Seisenberger – Swansea Sylvain Dailler – Lyon LIX, 18 January 2011 1 / 25

  • interesting extracted

  • extracted programs

  • related work

  • primitive predicate

  • predicate operators

  • constructive topping

  • ordered fields

  • coinductive definitions


Subjects

Informations

Published by
Reads 8
Language English

Exrait

Program extraction from proofs: computable analysis and parser generation
Ulrich Berger – Swansea
Joint work with
Monika Seisenberger – Swansea Sylvain Dailler – Lyon
LIX, 18 January 2011
1/25
Overview
Mathematical and formal framework
Natural and real numbers
Uniformly continuous
Monadic parsing
Related work
Conclusion
functions
2 / 25