Noam Zeilberger
email: [my full name] at gmail.com 
bitmessage: BM2cXzF3dZqCRzBVW56RbxJmiUL1gcw3ZXJw 
Background
I am currently a member of the Mathematical Components group at the MSRINRIA Joint Centre. Last year I participated in the special year on type theory at the IAS. Before that, I spent a year at the IMDEA Software institute in Madrid, and before that two years in Paris at Laboratoire PPS and Equipe πr², on a fellowship of the Fondation Sciences Mathématiques de Paris. I got my PhD in 2009 from CMU SCS, after six great years living in Pittsburgh.
Research Interests
I am interested broadly in the connections between
language and computation, and am excited by the potential of logic
for facilitating communication and reaching unity across different
disciplines. I have spent time thinking about the CurryHoward
correspondence in general, and more specifically about:
 continuations and computational duality
 the problem of sideeffects
 linear logic and focalisation
 type refinement and dependent types
 program termination/proof normalization
Recently, I have also become interested in the notion of
zeroknowledge from cryptography/complexity theory, and how it relates to
notions of knowledge from proof theory.
Recent drafts
 Type refinement and monoidal closed bifibrations.

With PaulAndré Melliès. October 1, 2013.
Recent talks
 Type refinement in the abstract.

October 16, 2013, at MSR Cambridge. [inkscape svg]
 Polarity in Proof Theory and Programming.

August 30, 2013, at the Summer School on Linear Logic and Geometry of Interaction in Torino, Italy.
 HOPE for a typetheoretic understanding of zeroknowledge.

September 9, 2012, at the 1st ACM SIGPLAN workshop on HigherOrder Programming with Effects. (Note: the slides seem to render funny with Firefox  best viewed in Chrome or Safari.)
BONUS: slides for
the "15 minute" version I gave October 4th at the IAS postdoc seminar series.
Older publications
 Polarity and the logic of delimited continuations.

In Proceedings of the TwentyFifth Annual IEEE Symposium on Logic in Computer Science (LICS 2010). [twelf code] [slides]
 Defunctionalizing focusing proofs.

Presented at the 2009 International Workshop on ProofSearch in Type Theories.
[twelf code] [more twelf]
 Refinement types and computational duality.

In Proceedings of the 2009 Workshop on Programming Languages meets Program Verification (PLPV 09). [agda code]
 Focusing on binding and computation.

With Dan Licata and
Bob Harper.
In Proceedings of the TwentyThird Annual IEEE Symposium on Logic in Computer Science (LICS 08).
[tech report]
 Focusing and higherorder abstract syntax.

In Proceedings of the 35th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 08).
[coq code] [notes]
 On the unity of duality.

Annals of Pure and Applied Logic 153:1 (2008), special issue on "Classical logic and computation". [doi]
Dissertation
PhD in computer science, 2009, Carnegie Mellon University
The Logical Basis of Evaluation Order and PatternMatching.
Committee:
Peter Lee (coadvisor),
Frank Pfenning (coadvisor),
Robert W. Harper,
PaulAndré Melliès (external member)
Techniques from linear logic and infinitary proof theory (connected to the old
idea of a "prooftheoretic semantics" of logic) yield new insights
into seemingly extralogical features of modern programming languages.
By applying the CurryHoward 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 builtin support for
patternmatching. This framework provides an elegant, uniform account of
both untyped and intrinsically welltyped computation, and moreover can
be extended with an extrinsic (Currystyle) 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.
Other papers
 Nathack: a natural language interface for nethack.

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.
Et cetera
 Wikipedia editing / the nLab
 Knowledge is a collaborative effort.
 And Quiet Flows the Mon
 A photography project from the dark days after the 2004 U.S. Presidential Elections.
 In Tune With Fun
 A truelife story about learning the accordion.
We may just be cockroaches at the base of a very large garbage mountain.
Dana Scott (on mathematics)