Randy Pollack (Senior Research Fellow)

Currently at Harvard University (2011-2012)

• My Curriculum Vitae (.pdf)

Recent papers

• A Canonical Locally Named Representation of Binding, Randy Pollack, Masahiko Sato and Wilmer Ricciotti
  • Making the Sato representation abstract.
  • Special issue of Journal of Automated Reasoning (DOI 10.1007/s10817-011-9229-y) .pdf
  • Isabelle files for this paper .tgz
  • Matita files for this paper .tgz
• External and Internal Syntax of the Lambda-calculus, Masahiko Sato and Randy Pollack,
  • Journal of Symbolic Computation 45 (2010) pp. 598-616 .pdf
  • Isabelle theory files formalizing the representation in this paper .tgz
• Engineering Formal Metatheory, Aydemir, Chargueraud, Pierce, Pollack and Weirich
  • POPL, 2008 .pdf
• Strong Induction Principles in the Locally Nameless Representation of Binders, Urban and Pollack
  • Workshop on Mechanized Metatheory (colocated with ICFP 2007) .pdf
• A Logical Framework with Dependently Typed Records, Thierry Coquand, Randy Pollack and Makoto Takeyama.
  • Fundamenta Informaticae 65(1-2), 2005 .ps.gz .pdf
• Reasoning About CBV Functional Programs in Isabelle/HOL, John Longley and Randy Pollack.
  • In TPHOLs 2004 .ps.gz .pdf

Harvard CS252r

• A bibliography of recent papers on binding .pdf.
• Slides about local representations of binding .pdf.
• Church--Rosser Theorem Slides in .pdf, Paper in .ps.gz
• Slides about Higher Order Abstract Syntax Slides in .pdf,
• Slides about Combinators, Deduction Theorem, and Normalization Slides in .pdf, Coq .v file, Coqdoc .html file,

Recent presentations

• A Canonical Locally Named Representation of Binding .pdf.
  • Talk at Scottish Theorem Proving meeting, 20/11/2009.
• A Canonical Locally Named Representation of Binding, in WMM'09 .pdf.
  • An abstract presentation of the work described in the TAASN'09 talk below.
  • Paper submitted to a special issue of Journal of Automated Reasoning..
• A Canonical Local Representation of Binding, in TAASN'09. .pdf.
  • Full paper to appear in J. Symbolic Computation.
  • Isabelle theory files formalizing the representation in this paper .tgz
• Local Representations of Binding .pdf
• The Constructive Engine .pdf
• Some Recent Logical Frameworks .pdf
• Reasoning About Languages with Binding .pdf

Other publications and older links

• bibtex and URLs
• Other documents available in my ftp directory
• The LEGO Proof Assistant home page
• Type Theory Course for PhD students, LFCS, Mar - Apr 2004.
• TYPES topical workshop "Math Wiki", 31 Oct - 1 Nov 2007.

Professional Activities

• Program committee of Interactive Theorem Proving (ITP 2012)
• Edinburgh site leader for EU project FET Open - FP7 ICT 243881 CerCo.
• Program committees of Workshop on Proof Search in Type Theories (PSTT'09) and Modules and Libraries for Proof Assistants (MLPA'09), both to be co-located with CADE'09 (Montreal).
• Program committee of Theorem Proving in Higher Order Logics (TPHOLs) 2009.
• Program committee of Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2008.
• Organising a TYPES, topical workshop Math Wiki in Edinburgh, 31/10 - 1/11 2007.
• Steering committee of EU Coordination Action 510996 (TYPES). (TYPES project page, Edinburgh TYPES site page).
• Program committee of Workshop on Mechanizing Metatheory (WMM) 2007.
• Program committee of Types in Language Design and Implementation (TLDI) 2007.
• Program committee of Programming Languages meets Program Verification (PLPV) 2006.
• Program committee of Workshop on Mathematically Structured Functional Programming (MSFP) 2006.
• Steering committee of MERLIN workshop (MEchanized Reasoning about Languages with varIable biNding).
• Program committee chair of MERLIN 2005 workshop.
• Co-organizer of by-invitation workshop Binding Challenges at JAIST (Kanazawa, Japan), Apr. 2005.
• Program committee of LFM'04 workshop (Logical Frameworks and Meta-Languages).