Liron Cohen, a former postdoctoral researcher in Computer Science at Cornell and currently Senior Lecturer at Ben-Gurion University, and Robert L. Constable, Professor of Computer Science in the Ann S. Bowers College of Computing and Information Science at Cornell, won the Amnon Pazy Memorial Research Award for Best 2021 United States-Israel Binational Science Foundation (BSF) Grant Proposal for “Extending and Applying Implemented Intuitionistic Mathematics.” The authors explain their award-winning research agenda:
Whereas standard mathematical discourse is based on classical mathematics, constructive mathematics offers a more computational approach which has been exploited widely in various applications in computer science. The variant of constructive mathematics called intuitionistic mathematics, is however less well-known and investigated despite its unique computational capabilities. Intuitionistic mathematics which originated in the ideas of Brouwer, extends the standard notion of computability by incorporating novel forms of computation that are not governed by any law (for example, ones generated by throwing a dice). However, despite considerable work on the theoretical foundations of Brouwer’s intuitionistic theory, it has not yet been studied in a formal, computational setting.
To fill this gap, the proposed study aims to develop a new mechanized tool for formal reasoning that fully integrates the extended notion of computation and use the unique resulting computational setting to explore the wider implications of the theory. We will then use the powerful resulting framework to develop novel intuitionistic mathematical theories, namely, intuitionistic calculus and intuitionistic homotopy theory.
Leveraging the novel computational capabilities is expected to have major implications, both theoretical and practical, across different areas. In particular, it will improve the capabilities of mechanized tools and facilitate significant advances in formal verification, make calculus more elegant and practical, and help physicists explore continuous phenomena.
The Pazy Award will provide the resources needed for Cohen and Constable to pursue their proposed research.
For related coverage of Professor Constable’s research at Cornell, including the Nuprl initiative, see “Something Missing in Euclid? Twenty-Five Centuries of Research Newly Informed by Cornell CS’ Nuprl Proof Assistant.”
Also, listen to The Type Theory Podcast interview, episode 5: “Bob Constable on CTT and Nuprl.”