[TYPES/announce] LCC 2017: 2nd call for papers; 1st call for participation

2017-03-28 Thread Norman Danner
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

==
 First Call for Participation
Second Call for Papers
   LCC 2017  
  18th International Workshop on Logic and Computational Complexity
  June 19, 2017, Reykjavik, Iceland
  collocated with LICS 2017
   http://www.cs.swansea.ac.uk/lcc/
==

LCC meetings are aimed at the foundational interconnections between logic and
computational complexity, as present, for example, in implicit computational
complexity (descriptive and type-theoretic methods); deductive formalisms as
they relate to complexity (e.g. ramification, weak comprehension, bounded
arithmetic, linear logic and resource logics); complexity aspects of finite
model theory and databases; complexity-mindful program derivation and
verification; computational complexity at higher type; and proof complexity.
The program will consist of invited lectures as well as contributed talks
selected by the Program Committee.  

IMPORTANT DATES:

 * submission April 14, 2017
 * notification   May1, 2017
 * workshop   June  19, 2017 

INVITED SPEAKERS:

 * Arnaud Durand, Université Denis Diderot - Paris 7
 * Damiano Mazza, Institut Galilée, Université Paris-Nord

SUBMISSION:

We welcome submissions of abstracts based on work submitted or published
elsewhere, provided that all pertinent information is disclosed at
submission time.  There will be no formal reviewing as is usually
understood in peer-reviewed conferences with published proceedings.  The
program committee checks relevance and may provide additional feedback.

Submissions must be in English and in the form of an abstract of about 3-4
pages.  All submissions should be submitted through Easychair at:

   https://easychair.org/conferences/?conf=lcc2017

PROGRAM COMMITTEE:

Norman Danner (co-chair, Wesleyan University, Connecticut, USA)
Heribert Vollmer (co-chair, Leibniz Universität, Hannover)
Martin Avanzini (Universität Innsbruck)
Olaf Beyersdorff (University of Leeds)
Juha Kontinen (University of Helsinki)
Ramyaa (New Mexico Tech)
James S. Royer (Syracuse University)
Cristina Sirangelo (Paris Diderot University - Paris 7)

REGISTRATION:

Registration for LiCS 2017 and LCC is now open, and early registration ends on
Friday, 07 April 2017.  To register, please visit

  http://lics.rwth-aachen.de/lics17

-- 
Norman Danner - ndan...@wesleyan.edu - http://ndanner.web.wesleyan.edu
Department of Mathematics and Computer Science  -  Wesleyan University 



[TYPES/announce] CFP: ML Family Workshop 2016

2017-03-28 Thread Sam Lindley

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

--
  CALL FOR PAPERS

  ML Family Workshop 2017
7 September 2017, Oxford, UK

  http://www.mlworkshop.org/ml2017/
   (co-located with ICFP)
--

ML is a family of programming languages that includes Standard ML,
OCaml, F#, SML#, Manticore, MetaOCaml, JoCaml, Alice ML, Dependent ML,
Flow Caml, and many others. All ML languages share several fundamental
traits, besides a good deal of syntax. They are higher-order, strict,
mostly pure, and typed, with algebraic and other data types. Their
type systems are derived from Hindley-Milner. The development of these
languages has inspired a significant body of computer science research
and influenced the design of many other programming languages,
including Haskell, Rust, and Scala.

ML workshops have been held in affiliation with ICFP continuously
since 2005. This workshop specifically aims to recognise the entire
extended ML family and to provide a forum for presenting and
discussing common issues, both practical (compilation techniques,
implementations of concurrency and parallelism, programming for the
Web) and theoretical (fancy types, module systems,
metaprogramming). The scope of the workshop includes all aspects of
the design, semantics, theory, application, implementation, and
teaching of the members of the ML family. We also encourage
presentations from related languages (such as ATS, Eff, F*, Koka,
Links, Rust, Scala, Swift, etc.), to exchange experience of further
developing ML ideas. Last year's ML Family workshop included talks
covering eight different ML dialects and related languages: Eff, F#,
F*, Links, Manticore, OCaml, SML, and SML#.

The ML family workshop will be held in close coordination with the
OCaml Users and Developers Workshop.

Invited speaker
---

Edwin Brady (University of St Andrews, UK)

Scope
-

We acknowledge the whole breadth of the ML family and aim to include
languages that are closely related, such as Rust and Scala. Those
languages have implemented and investigated run-time and type system
choices that may be worth considering for OCaml, F# and other ML
languages. We also hope that the exposure to state of the art ML might
favourably influence those related languages. Specifically, we seek
research presentations on topics including (but not limited to):

  * Language design: abstraction, higher forms of polymorphism,
concurrency, distribution and mobility, staging, extensions for
semi-structured data, generic programming, object systems, etc.

  * Implementation: compilers, interpreters, type checkers, partial
evaluators, runtime systems, garbage collectors, foreign function
interfaces, etc.

  * Type systems: inference, effects, modules, contracts,
specifications and assertions, dynamic typing, error reporting,
etc.

  * Applications: case studies, experience reports, pearls, etc.

  * Environments: libraries, tools, editors, debuggers, cross-language
interoperability, functional data structures, etc.

  * Semantics: operational and denotational semantics, program
equivalence, parametricity, mechanization, etc.

Four kinds of submissions will be accepted: Research Presentations,
Experience Reports, Demos and Informed Positions.

  * Research Presentations: Research presentations should describe new
ideas, experimental results, or significant advances in ML-related
projects. We especially encourage presentations that describe work
in progress, that outline a future research agenda, or that
encourage lively discussion. These presentations should be
structured in a way which can be, at least in part, of interest to
(advanced) users.

  * Experience Reports: Users are invited to submit Experience Reports
about their use of ML and related languages. These presentations
do not need to contain original research but they should tell an
interesting story to researchers or other advanced users, such as
an innovative or unexpected use of advanced features or a
description of the challenges they are facing or attempting to
solve.

  * Demos: Live demonstrations or short tutorials should show new
developments, interesting prototypes, or work in progress, in the
form of tools, libraries, or applications built on or related to
ML and related languages. (You will need to provide all the
hardware and software required for your demo; the workshop
organisers are only able to provide a projector.)

  * Informed Positions: A justified argument for or against a language
feature. The argument must be substantiated, either theoretically
(e.g. by a demonstration of (un)soundness, an inference 

[TYPES/announce] Categories Logic and Physics Scotland 5 April 2017

2017-03-28 Thread Chris Heunen
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

CATEGORIES LOGIC AND PHYSICS SCOTLAND
Wednesday 5 April 2017
Department of Computer and Information Sciences, University of Strathclyde
http://homepages.inf.ed.ac.uk/cheunen/clapscotland/

Following our successful meetings last year, we are pleased to announce the
third workshop in the CLAP Scotland series, and invite you to participate.

Programme:
* Kevin Dunne (University of Strathclyde):
  "Infinite-Dimensional Categorical Quantum Mechanics, Spectra, and
Contextuality"
* Chris Heunen (University of Edinburgh):
  "The category of Hilbert modules"
* Peter Hines (University of York):
  "Diagrams and Coherence Theorems in Cryptography and Cryptanalysis"
* Aleks Kissinger (Radboud University):
  "A categorical semantics for causal structure"
* Clemens Kupke (University of Strathclyde):
  "Games for topological fixpoint logics"
* Fabio Zanasi (University College London):
  "A new foundation for string diagram rewriting: adequacy, confluence,
commutativity"

Registration is free. For catering purposes, please email the local
organiser  as soon as possible if you plan to
attend.

Best wishes,
Chris Heunen and Ross Duncan
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.


[TYPES/announce] CFP: Encyclopedia of Proof Systems

2017-03-28 Thread Giselle Reis
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

== EPS ==
Encyclopedia of Proof Systems

 --- call for contributions ---

September 24-25, 2017, Brasilia, Brazil

Affiliated to:
TABLEAUX, FroCoS and ITP 2017
http://tableaux2017.cic.unb.br/
http://frocos2017.cic.unb.br/
http://itp2017.cic.unb.br/


Aims and Scope
==

The Encyclopedia of Proof Systems was created in 2014 with the goal of
being a quick reference for the various proof systems used by
logicians. Since then, it has collected 64 entries on the most various
logics and calculi. This was only possible due to the collaboration of
many members of the logic community.

This event aims to promote the encyclopedia and attract more
contributions and collaborators. It consists of:

- a poster session in the afternoon of September 24th, 2017, during
  which submitted entries will be displayed as posters;

- an interactive hands-on meeting in the morning of September 25th,
  2017, for those who would like to contribute to the continuous
  improvement of the encyclopedia.

The activities planned for this meeting will be announced closer to
the event.


Submission Instructions
===

Please visit the task-force's website for instructions:
http://proofsystem.github.io/Encyclopedia

Participation in TABLEAUX, FroCoS or ITP is not required for
submission, but is strongly encouraged.


Important Dates
===

- Submission Deadline: 1st of August 2017
- Notification: 15th of August 2017


Publication Plans
=

We have an agreement with College Publications to publish the
encyclopedia as a book. The first edition, containing the entries
submitted until 2016, was published on January 2017
(http://www.collegepublications.co.uk/other/?00028).

Future editions will contain the entries submitted for this EPS event.
The encyclopedia is also available in Github
(https://github.com/ProofSystem/Encyclopedia).


Organization


Bruno Woltzenlogel Paleo (bruno...@gmail.com)
Giselle Reis (gise...@cmu.edu)


[TYPES/announce] Second call for papers: QPL 2017

2017-03-28 Thread Aleks Kissinger
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

 SECOND CALL FOR PAPERS

 The 14th International Conference on
  Quantum Physics and Logic (QPL)

July 3-7, 2017
  Radboud Universiteit, Nijmegen, Netherlands

  http://qpl.cs.ru.nl


SUBMISSION DEADLINE: 21 April, 2017

The 14th International Conference on Quantum Physics and Logic (QPL)
will take place at Radboud University between Monday 3 and
Friday 7 July, 2017.

The conference brings together researchers working on mathematical
foundations of quantum physics, quantum computing, and related areas,
with a focus on structural perspectives and the use of logical tools,
ordered algebraic and category-theoretic structures, formal languages,
semantical methods, and other computer science techniques applied to
the study of physical behaviour in general. Work that applies
structures and methods inspired by quantum theory to other fields
(including computer science) is also welcome.

Previous QPL events were held in Glasgow (2016), Oxford (2015),
Kyoto (2014), Barcelona (2013), Brussels (2012), Nijmegen (2011),
Oxford (2010), Oxford (2009), Reykjavik (2008), Oxford (2006),
Chicago (2005), Turku (2004), and Ottawa (2003).


REGISTRATION IS NOW OPEN!

Find registration details via the QPL 2017 website or register
directly at:

https://rudigitalsecurity.paydro.com/qpl-2017


SATELLITES

There will be a satellite workshop on Quantum Structures hosted by the
International Quantum Structures Association (IQSA) from Tuesday July
4th to Friday the 7th. See the QPL website for more information. A
separate call for abstracts and participation will be issued shortly.


JOINT QPL-IQSA INVITED SPEAKER

Miriam Backens (Bristol)


QPL INVITED SPEAKERS

Matthias Christandl (Copenhagen)
Miguel Navasques (Vienna)
Paulo Perinotti (Pavia)
Jamie Vicary (Oxford)


QPL INVITED TUTORIALS

Bart Jacobs (Radboud) - Effectus Theory
Dan Marsden (Oxford) - Categorical String Diagrams
Simon Perdrix (LORIA) - Measurement-based Quantum Computation
Ronald de Wolf (CWI) - Quantum Algorithms



IMPORTANT DATES

Submission: 21 April, 2017
Notification: 29 May
Papers ready: 23 June
Conference: 3-7 July



SUBMISSIONS

Prospective speakers are invited to submit a contribution to the
conference.

 - Original contributions consist of a 5-12 page extended abstract
   which provides sufficient evidence of results of genuine interest
   and enough detail to allow the program committee to assess the
   merits of the work. Submission of substantial albeit partial
   results of work in progress is encouraged. Authors of accepted
   papers will be invited to give long or short talks, depending on
   the quality and/or maturity of the submission.

 - Extended abstracts describing work submitted/published elsewhere
   will also be considered, provided the work is recent and relevant
   to the conference. These consist of a 3 page description and should
   include a link to a separate published paper or preprint.


Extended versions of accepted original research contributions will be
published in Electronic Proceedings in Theoretical Computer Science
(EPTCS) after the conference.

Submissions should be prepared using LaTeX, and must be submitted
in PDF format. Use of the EPTCS style is encouraged. Submission is
done via EasyChair:

https://www.easychair.org/conferences/?conf=qpl2017

There will be an award for the best paper whose authors are all
students, at the discretion of the programme committee.


PROGRAMME COMMITTEE

Aleks Kissinger (Radboud, co-chair)
Bob Coecke (Oxford, co-chair)

Samson Abramsky (Oxford)
Miriam Backens (Bristol)
John Baez (UC Riverside)
Benno van den Berg (Amsterdam)
Rick Blute (Ottawa)
Dan Browne (University College London)
Giulio Chiribella (Hong Kong)
Ross Duncan (Strathclyde)
Simon Gay (Glasgow)
Chris Heunen (Edinburgh)
Matty Hoban (Oxford)
Dominic Horsman (Durham)
Bart Jacobs (Radboud)
Kohei Kishida (Oxford)
Joachim Kock (Barcelona)
Matt Leifer (Chapman)
Hans Maassen (Radboud)
Paul-Andre Mellies (Paris Diderot)
Michael Moortgat (Utrecht)
Daniel Oi (Strathclyde)
Prakash Panangaden (McGill)
Dusko Pavlovic (Hawaii)
Simon Perdrix (CNRS Nancy)
Paolo Perinotti (Pavia)
Robert Raussendorf (British Columbia)
Lidia del Rio (ETH Zurich)
Ana Belen Sainz (Perimeter Institute)
Peter Selinger (Dalhousie)
Pawel Sobocinski (Southampton)
Rob Spekkens (Perimeter Institute)
Isar Stubbe (Littoral-Cote-d'Opale)
Benoit Valiron (Paris-Sud)
Jamie Vicary (Oxford)
Mingsheng Ying (UT Sydney)


STEERING COMMITTEE

Bob Coecke (Oxford)
Prakash Panangaden (McGill)
Peter Selinger (Dalhousie)


LOCAL ORGANISATION

Bart Jacobs
Aleks Kissinger
Sander Uijlen


[TYPES/announce] CFP: Workshop on Type-driven Development (TyDe '17)

2017-03-28 Thread Sam Lindley

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


CALL FOR PAPERS

2nd Workshop on Type-Driven Development (TyDe '17)
 3 September 2017, Oxford, UK

 http://tydeworkshop.org/2017


# Goals of the workshop

The workshop on Type-Driven Development aims to show how static type
information may be used effectively in the development of computer
programs. Co-located with ICFP, this workshop brings together leading
researchers and practitioners who are using or exploring types as a
means of program development.

We welcome all contributions, both theoretical and practical, on a
range of topics including:

-   dependently typed programming;
-   generic programming;
-   design and implementation of programming languages, exploiting types
in novel ways;
-   exploiting typed data, data dependent data, or type providers;
-   static and dynamic analyses of typed programs;
-   tools, IDEs, or testing tools exploiting type information;
-   pearls, being elegant, instructive examples of types used in the
derivation, calculation, or construction of programs.

# Program Committee

-   Nada Amin, EPFL, Switzerland
-   Ana Bove, Chalmers University of Technology, Sweden
-   Patricia Johann, Appalachian State University, US
-   Yukiyoshi Kameyama, University of Tsukuba, Japan
-   Sam Lindley, The University of Edinburgh, UK (co-chair)
-   Limin Jia, CMU, US
-   Assia Mahboubi, INRIA Saclay, France
-   Liam O’Connor, University of New South Wales, Australia
-   Nicolas Oury, Jane Street, UK
-   Jennifer Paykin, University of Pennsylvania, US
-   Paula Severi, University of Leicester, UK
-   Tarmo Uustalu, Talinn University of Technology, Estonia
-   Jeremy Yallop, University of Cambridge, UK
-   Brent Yorgey, Hendrix College, US (co-chair)

# Proceedings and Copyright

We plan to have formal proceedings, published by the ACM. Accepted
papers will be included in the ACM Digital Library. Authors must grant
ACM publication rights upon acceptance, but may retain copyright if they
wish. Authors are encouraged to publish auxiliary material with their
paper (source code, test data, and so forth). The proceedings will be
freely available for download from the ACM Digital Library from one week
before the start of the conference until two weeks after the conference.

# Submission details

Submissions should fall into one of two categories:

-   Regular research papers (12 pages)
-   Extended abstracts (2 pages)

The bibliography will not be counted against the page limits for
either category.

Regular research papers are expected to present novel and interesting
research results, and will be included in the formal
proceedings. Extended abstracts should report work in progress that
the authors would like to present at the workshop. Extended abstracts
will be distributed to workshop attendees but will not be published in
the formal proceedings.

We welcome submissions from PC members (with the exception of the two
co-chairs), but these submissions will be held to a higher standard.

Submission is handled through HotCRP:

  https://icfp-tyde17.hotcrp.com/

All submissions should be in portable document format (PDF) and
formatted using the ACM SIGPLAN style guidelines:

  http://www.sigplan.org/Resources/Author/

*Note* that the ACM SIGPLAN style guidelines have changed from
previous years!  In particular, submissions should use the new
'acmart' format and 'sigplan' subformat.

Extended abstracts must be submitted with the label 'Extended
abstract' clearly in the title.

# Important Dates

-   Regular paper deadline: Wednesday, 24th May, 2017
-   Extended abstract deadline: Wednesday, 7th June, 2017
-   Author notification: Wednesday, 28th June, 2017
-   Deadline for camera ready version: Saturday, 15th July, 2017
-   Workshop: Sunday, 3rd September, 2017

# Travel Support

Student attendees with accepted papers can apply for a SIGPLAN PAC grant
to help cover travel expenses. PAC also offers other support, such as
for child-care expenses during the meeting or for travel costs for
companions of SIGPLAN members with physical disabilities, as well as for
travel from locations outside of North America and Europe. For details
on the PAC program, see its web page:

  http://www.sigplan.org/PAC/

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.