Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Noam Zeilberger
I am interested in programming languages and logic, and the
connection between them known as the propositions-as-types
correspondence (or proofs-as-programs, or Curry-Howard, etc.).
I am especially interested in type systems that
push the boundaries of this correspondence, such as dependent types
and refinement types. More generally, I am interested in the
interaction of syntax and semantics, in programming languages as
well as proof theory, model theory, and games semantics. I use
proof assistants (such as Agda, Coq, and Twelf) as mathematical
laboratories for experimenting with ideas. I believe that a close
connection between theory and practice is both possible and
necessary.
Techniques from linear logic and infinitary proof theory (connected to the old
idea of a "proof-theoretic semantics" of logic) yield new insights
into seemingly extra-logical features of modern programming languages.
By applying the Curry-Howard correspondence to focusing proofs,
we develop a polarized type theory in which evaluation order is
explicitly reflected at the level of types, and which has built-in support for
pattern-matching. This framework provides an elegant, uniform account of
both untyped and intrinsically well-typed computation, and moreover can
be extended with an extrinsic (Curry-style) type system to express
and enforce more refined semantic properties of programs. We
apply these ideas to explore the theory of typing and subtyping for
intersection and union types in the presence of effects, giving a
simplified explanation of some of the unusual artifacts of existing systems.
August, 2005. An attempt at a constructive proof of the soundness of labelled deduction for intuitionistic logic. This is essentially a variation on the usual "prime context" approach establishing completeness of intuitionistic logic with respect to Kripke semantics, but avoiding proof-by-contradiction, and using the subformula property to stay finitary. For a more novel approach, see Jason Reed and Frank Pfenning's "Intuitionistic letcc via labelled deduction".
June, 2005. Describes how to extend the logic of bunched implications with an S4-like box modality, and its relationship to "purity" in separation logic.
January, 2003. With Cassia Martin, David Molnar, and Dev Purkayastha. As the title suggests,
this was a natural language interface for nethack! Done with a mix of prolog, embedded lua, and
scary hacking within nethack's internal C source. Our code is lying around
somewhere, and I could dig it up upon request.
On Dummett's invitation, Martin-Löf gave a series of eight lectures
at Oxford's All Souls College, with Dummett and Dag Prawitz in the audience.
This letter (dated shortly before Dummett's 1976 William
James Lectures) was accompanied by Peter Hancock's notes on the
first half of this series. Thanks to Peter Hancock for the scanned copy.