The continuity of monadic stream functions

Capretta, Venanzio; Fowler, Jonathan

Abstract

© 2017 IEEE. Brouwer's continuity principle states that all functions from infinite sequences of naturals to naturals are continuous, that is, for every sequence the result depends only on a finite initial segment. It is an intuitionistic axiom that is incompatible with classical mathematics. Recently Martín Escardó proved that it is also inconsistent in type theory.

Citation

Capretta, V., & Fowler, J. (2017, June). The continuity of monadic stream functions. Presented at 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland

• Presentation Conference Type: Edited Proceedings
• Conference Name: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Start Date: Jun 20, 2017
• End Date: Jun 23, 2017
• Acceptance Date: Mar 22, 2017
• Online Publication Date: Aug 10, 2017
• Publication Date: 2017-06
• Deposit Date: Sep 18, 2017
• Publicly Available Date: Sep 18, 2017
• Publisher: Institute of Electrical and Electronics Engineers
• Pages: 658-669
• Series Title: Annual Symposium on Logic in Computer Science
• Series ISSN: 1043-6871
• Book Title: Proceedings - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
• ISBN: 9781509030194
• DOI: https://doi.org/10.1109/LICS.2017.8005119
• Keywords: monadic stream function, continuity, type theory functional programming, stream, monad, dialogue trees, strategy trees
• Public URL: https://nottingham-repository.worktribe.com/output/878125
• Publisher URL: https://ieeexplore.ieee.org/document/8005119
• Related Public URLs: http://lics.rwth-aachen.de/lics17/
• Additional Information: © 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.