New York University

Computer Science Department

Courant Institute of Mathematical Sciences

  Car Collection
  Selected Drawings
  Mazda Promo
  Play Demo Poker
Academic Interests:

Relations Between Mathematical Logic and Computation

Program Specifications and their Proofs

The Curry—Howard Isomorphism and Type Theory

Asymptotic Analysis of Programs


Semantics of Partial Functions (view on rg.png)

Decision Procedure for a Theory of Inductive Data Types (view on rg.png)

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (view on rg.png)

(More coming soon)

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)

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

Student Conferences and Summer Schools:

New York Graduate School Logic Conference, St. Francis College.

Fields Institute Summer School on Logic and Foundation of Computation, Ottawa, Canada.

Conference on Verification, Model Checking and Abstract Interpretation. New York.

Proofs as Programs Summer School. Eugene, Oregon.

Summer School on Logical Methods. Aarhus, Denmark.

Student Conference on Mathematics and Physics, Sneek, Fryslând, Amstermdam, The Netherlands.

Student Exchange Program, München, Berlin, Germany.