Randy Pollack (Research Assistant, Honorary Fellow)

• My Curriculum Vitae (.pdf)

PhD post available

• 3 year funded position. Contact me.
• EU funded project CERCO; a certified complexity preserving compiler.
• Cost models, semantics, executable compiler and correctness proofs all in dependent type theory.
• Project partners: Edinburgh, University of Bologna and University Paris 7 Laboratoire PPS.

Recent papers

• A Canonical Locally Named Representation of Binding, Randy Pollack and Masahiko Sato
  • Making the Sato representation abstract.
  • Submitted to a special issue of Journal of Automated Reasoning. .pdf
  • Isabelle files for this paper .tgz
• External and Internal Syntax of the Lambda-calculus, Masahiko Sato and Randy Pollack
  • To appear in Journal Symbolic Computetion .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

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

• 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).