Workshop on Coalgebra, Horn Clause Logic Programming and Types

Edinburgh, UK, 28–29 November 2016

The workshop marks the end of the EPSRC Grant Coalgebraic Logic Programming for Type Inference, by K. Komendantskaya and J. Power and will consist of two parts:

Part 1
Semantics: Lawvere theories and Coalgebra in Logic and Functional Programming
Part 2
Programming languages: Horn Clause Logic for Type Inference in Functional Languages and Beyond

We invite all colleagues working in related areas to present and share their results. We envisage a friendly meeting with many stimulating discussions, and therefore welcome presentations of already published research as well as novel results. Authors of original contributions will be invited to submit their papers to EPTCS post-proceedings. We especially encourage early career researchers to present and participate.

Venue: The workshop will be held at the International Centre for Mathematical Sciences , in Edinburgh city centre, just 2 minutes walk from the Informatics Forum, please see the map.

Semantics: Lawvere theories and Coalgebra in Logic and Functional Programming

Over recent years, there has been considerable research on the semantics of operational aspects of logic programming. The underlying mathematics has often involved coalgebra on a presheaf category or a variant of a presheaf category, with index given by the Lawvere theory generated by a signature. That has much in common with many years of research on the semantics of functional programming.

The combination of coalgebra with Lawvere theories has already led to applied development, and there seems good reason to hope that that will continue, with application to logic and functional programming both separately and in combination with each other. So we would like to spend a few days bringing researchers in the area together to compare the techniques they are developing and the problems they are addressing.

Our semantic investigations led to analysis of theorem proving, and that was reciprocated, with theorem proving further influencing our semantics. Theorem proving in turn led us to study type inference, leading to the central applied focus of our work, thus the second topic of the workshop.

Programming languages: Horn Clause Logic for Type Inference in Functional Languages and Beyond

We will aim to identify challenges in type inference in various domains and facilitate the research communities to collaboratively seek for effective methods, primarily focusing on Logic Programming (LP), in a broad sense, which includes resolution-based systems, constraint solving, automated and interactive theorem provers. The term "type inference" is also used in a broad sense including all three directions of type related computations: type checking, type inference, and type inhabitation.

The topics of interest include but are not limited to:

  • deriving implementations and/or proofs from declarative specifications of type systems,
  • identifying challenges and/or introducing approaches on type inference for non-traditional type systems (e.g., gradual/hybrid typing, success typing, types for process calculus, ...),
  • innovative ideas and new/old theories of LP that could benefit type inference,
  • integration of LP methods within other parts of language systems and tools, and
  • adding/enhancing support for type inference in LP systems themselves.

Pre-proceedings

Pre-proceedings booklet is avalaible via arXiv.

Submission Details

We are now inviting all researchers in the relevant areas to submit original research papers to EPTCS workshop post-proceedings. These submissions will be peer-reviewed according to EPTCS standards by the workshop PC members.

The details are as follows:

  • All submissions must be made via Easychair, using the CoALP-Ty'16 submission site (please replace the your submission with a new version in case you submited an abstract for pre-proceedings).
  • The deadline for full papers is 1 March 2017 (now extended).
  • The page limit is 15 pages, including references. Any additional materials can be given in appendices.
  • Submissions must be formattred in the EPTCS style

Important Dates

Extended Abstract Submission
15 October, 2016
Author notification
25 October, 2016
Workshop registration
1 November, 2016  5 November, 2016
Workshop
28–29 November, 2016
EPTCS proceedings invitations
15 December, 2016
EPTCS proceedings abstracts
5 January, 2017
EPTCS final version submission
31 January, 2017  1 March, 2017 (extended)

Post-Proceedings Publication

The post-proceedings volume will be published in Electronic Proceedings in Theoretical Computer Science and peer-reviewed according to EPTCS standards by the PC members.

Programme

Monday 28 November

9:10 - 9:30
Registration
9:30 - 9:40
Welcome to CoALP-Ty'16
Ekaterina Komendantskaya (Heriot-Watt University)
9:40 - 11:10
Invited talk I
John Power (University of Bath)
Logic Programming: Laxness and Saturation
11:10 - 11:30
Coffee break
11:30 - 12:00
Contributed talk
Martin Schmidt: Coalgebraic Logic Programming: Implementation and Optimization
12:00 - 13:00
Invited talk II
Steven Ramsay and Luke Ong (University of Oxford)
Refinement Types and Higher-Order Constrained Horn Clauses
13:00 - 14:00
Lunch
14:00 - 15:00
Invited talk III
Tarmo Uustalu (Tallinn University of Technology)
Comodels and Interaction
15:00 - 15:30
Coffee break
15:30 - 17:00
Contributed talks
František Farka: Proofs by Resolution and Existential Variables
Bashar Igried and Anton Setzer: Defining Trace Semantics for CSP-Agda
Henning Basold and Ekaterina Komendantskaya: Models of Inductive-Coinductive Logic Programs
18:00 - 20:00
Workshop dinner
Lebanese restaurant Beirut, please see the map.
The dinner is not sponsored by the workshop

Tuesday 29 November

9:30 - 10:30
Invited talk IV
Claudio Russo (Microsoft Research), Matt Windsor (University of York), Don Syme (Microsoft Research), Rupert Horlick and James Clarke (University of Cambridge)
Classes for the Masses
10:30 - 11:00
Contributed talk
J. Garrett Morris: Semantical Analysis of Type Classes
11:00 - 11:30
Coffee break
11:30 - 12:30
Invited talk V
Davide Ancona (University of Genoa)
Abstract Compilation for Type Analysis of Object-Oriented Languages
12:30 - 13:30
Lunch
13:30 - 14:30
Invited talk VI
Ki Yung Ahn (Nanyang Technological University)
Relational Specification of Type Systems Using Logic Programming
14:30 - 15:15
Discussion panel
Q&A with invited speakers
15:15 - 15:45
Cofee break
15:45 - 16:45
Contributed talks
Clemens Kupke: Coalgebra and Ontological Rules
Luca Franceschini, Davide Ancona and Ekaterina Komendantskaya: Structural Resolution for Abstract Compilation of Object-Oriented Languages

Organising Committee

Workshop Chairs
Ekaterina Komendantskaya, Heriot-Watt University, UK
John Power, University of Bath, UK
Publicity Chair
František Farka, University of Dundee, UK and University of St Andrews, UK

Programme Committee

Ki Yung Ahn Nanyang Technological University, Singapore
Davide Ancona University of Genoa, Italy
Filippo Bonchi CNRS, ENS de Lyon, France
Iavor Diatchki Galois, Inc, USA
Peng Fu Heriot-Watt University, Edinburgh, UK
Neil Ghani University of Strathclyde, UK
Patricia Johann Appalachian State University, USA
Ekaterina Komendantskaya Heriot-Watt University, Edinburgh, UK
Clemens Kupke University of Strathclyde, UK
J. Garrett Morris University of Edinburgh, UK
Fredrik Nordvall Forsberg University of Strathclyde, UK
John Power University of Bath, UK
Claudio Russo Microsoft Research Cambridge, UK
Martin Schmidt Osnabrück University , Germany
Stephan Schulz DHBW Stuttgart, Germany
Aaron Stump The University of Iowa, USA
Niki Vazou University of California, San Diego, USA
Joe Wells Heriot-Watt University, Edinburgh, UK
Fabio Zanasi University College London, UK

Participants

Danel AhmanUniversity of Edinburgh, UK
Ki Yung AhnNanyang Technological University, Singapore
Davide AnconaUniversity of Genoa, Italy
Henning BasoldRadboud University, The Netherlands
Lukas ConventUniversity of Edinburgh, UK
František FarkaUniversity of Dundee, UK and University of St Andrews, UK
Luca FranceschiniUniversity of Genoa, Italy
Rik HowardBirkbeck, University of London, UK
Bashar Igried Deb AlkhawaldehSwansea University, UK
Martti KarvonenUniversity of Edinburgh, UK
Katya KomendantskayaHeriot-Watt University, Edinburgh, UK
Clemens KupkeUniversity of Strathclyde, UK
Xue LiUniversity of Edinburgh, UK
Yue LiHeriot-Watt University, Edinburgh, UK
Sam LindleyUniversity of Edinburgh, UK
Manuel MaarekHeriot-Watt University, Edinburgh, UK
Dan MarsdenUniversity of Oxford,UK
James McKinnaUniversity of Edinburgh, UK
Martin MöhrmannUniversity of Osnabrueck, Germany
Garrett MorrisUniversity of Edinburgh, UK
Dominic MulliganUniversity of Cambridge, UK
Luke OngUniversity of Oxford, UK
Christos PerivolaropoulosUniversity of Edinburgh, UK
John PowerUniversity of Bath, UK
Steven RamsayUniversity of Oxford, UK
Claudio RussoMicrosoft Research Cambridge, UK
Ankit ShuklaVIT University, India
Tarmo UustaluTallinn University of Technology, Estonia
Joe WellsHeriot-Watt University, Edinburgh, UK
Fabio ZanasiUniversity College London, UK

Sponsored by