Relations Between Mathematical Logic and Computation

Program Specifications and their Proofs

The Curry—Howard Isomorphism and Type Theory

Asymptotic Analysis of Programs

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

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)