
Academic Interests:
Relations Between Mathematical Logic and Computation
Program Specifications and their Proofs
The Curry—Howard Isomorphism and Type Theory
Asymptotic Analysis of Programs
Current Math Projects:
Ordinal Numbers as Programs (with Applications to Computational Lower Bounds)
Proofs by Transit via Meta Level (Meta Status of Deductively Undecidable Logical Propositions)
Dependent Conditional Operator for Disjunctive Data Types (Branching as Dynamic Dispatch)
Algebraic Types as Topological Spaces under Continuous Morphisms
Structure of Decidable Subsets under Computable Permutations of Countable Domains
Current Web Design Projects: