New York University

Computer Science Department

Courant Institute of Mathematical Sciences

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:

Polymorphic DataBase Concept for Java Enabled Servers

Automatic Deduction for Theories of Algebraic Data Types

Synthesis of Proofs from Types (Calculus of GUI Windows for Theorem Provers)