On Preserving the Computational Content of Mathematical Proofs: Toy Examples for a Formalising Strategy
- 2 July 2021
- book chapter
- Published by Springer Nature
- p. 285-296
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting StartedJahresbericht der Deutschen Mathematiker-Vereinigung, 2020
- PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS2019
- 2018 NORTH AMERICAN ANNUAL MEETING OF THE ASSOCIATION FOR SYMBOLIC LOGIC Western Illinois University, Macomb, IL, USA May 16–19, 2018The Bulletin of Symbolic Logic, 2018
- Opinion: The Mechanization of MathematicsNotices of the American Mathematical Society, 2018
- New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroupsJournal of Logic and Analysis, 2018
- Effective Rates of Convergence for the Resolvents of Accretive OperatorsNumerical Functional Analysis and Optimization, 2017
- Effective asymptotic regularity for one-parameter nonexpansive semigroupsJournal of Mathematical Analysis and Applications, 2016
- Rates of convergence and metastability for abstract Cauchy problems generated by accretive operatorsJournal of Mathematical Analysis and Applications, 2015
- Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximationAnnals of Pure and Applied Logic, 1993
- Finding computational content in classical proofs1991