Michal J. Gajda

Traditional explorations of Lambda Calculus typically initiate with a foundation in mathematical logic. However, the approach this talk takes is unique. It begins with a functional programming language, enhancing it progressively until it achieves totality, boundedness, bounded Turing completeness, and alignment with consistent ultrafinitist logic.

Along this intriguing journey, attendees will gain insights into the distinction between bounded total functions and mathematical proofs. Further, they will learn how to construct a tactic-based theorem prover and discover innovative methods to make logics significantly more appealing to the programming community. This talk promises to be both professionally enriching and engaging, providing fresh perspectives on well-established concepts.