Why $\lambda$‽

I am currently advertising two PhD studentships, on topics spanning programming languages, provenance, and data management, to start in fall 2016.

Both of these studentships are fully funded for applicants of any nationality (in contrast to many UK PhD studentships which are only funded up to the UK/EU tuition level, and do not cover full tuition fees for students from outside the European Union.)
Read more »

Labels: advertising, bidirectional computation, databases, functional programming, logic programming, programming languages, provenance

PPDP 2014

I attended PPDP 2014, in Canterbury, England a few weeks ago. Some notes about papers of interest there:


Read more »

Labels: functional reactive programming, logic programming, trip report

Programming with Higher-Order Logic
Dale Miller and Gopalan Nadathur
Cambridge University Press 2013

Church's higher-order logic, based on the typed $\lambda$-calculus, is a foundation of mathematics and computer science. It underpins a number of other influential logics and type theories, including systems for formalized mathematics such as LF, HOL and Coq, which in turn have led to interesting developments relevant to mainstream mathematics such as formal proofs of the Four-Color Theorem and Feit-Thompson Theorem in Coq, as well as the Homotopy Type Theory program initiated by Voevodsky. This book is about higher-order logic viewed in a different light, as a foundation for programming, specifically following the computation-as-deduction approach taken in logic programming languages such as Prolog. Higher-order logic programming builds on higher-order unification, and generalizes Horn clauses over first-order terms in Prolog to hereditary Harrop formulas over higher-order terms in languages such as $\lambda$Prolog. One might view (higher-order) logic programming as a tool deserving a place in a logician's toolbox analogous to numerical or symbolic tools for analysis: not a replacement for mathematical reasoning, but a framework for experimentation and automation.

Read more »

Labels: book review, higher-order logic, logic programming