Thomas Wahl | 2 Mar 00:05 2015

Formal Methods in Computer-Aided Design (FMCAD), 2015 - First Call for Papers


International Conference on
Formal Methods in Computer-Aided Design (FMCAD)

Austin, Texas, USA, September 27-30, 2015

** Note: ** FMCAD 2015 will be held at the end of September,
             several weeks earlier than in previous years!


FMCAD will be co-located with the SAT conference, and with the DIFTS and
ACL2 workshops. The conference program will include, in addition to regular
paper presentations, tutorials by Isil Dillig (UT Austin), Priyank Kalla
(Utah), and Andre Platzer (CMU), among others; new editions of the Hardware
Model Checking competition and the FMCAD Student Forum; an industrial panel
discussion; and keynote talks.

A small number of outstanding FMCAD submissions will be considered for
inclusion in a Special Issue of the journal on Formal Methods in System

FMCAD 2015 has technical co-sponsorship from the IEEE Council on Electronic
Design Automation, and in-cooperation status with ACM SIGPLAN (Special
Interest Group on Programming Languages) and ACM SIGSOFT (Special Interest
Group on Software Engineering).

(Continue reading)

Tarmo Uustalu | 27 Feb 18:33 2015

TYPES 2015 final call for contributions

[Selection of talks is based on abstracts (2 pp easychair.cls) 
due 13 March 2015! 

A post-proceedings volume in LIPIcs, with an open call.]

                       CALL FOR CONTRIBUTIONS

    21st International Conference on Types for Proofs and Programs,
                             TYPES 2015
                  Tallinn, Estonia,  18-21 May 2015



The TYPES meetings are a forum to present new and on-going work in all
aspects of type theory and its applications, especially in formalized
and computer assisted reasoning and computer programming. The meetings
from 1990 to 2008 were annual workshops of a sequence of five EU
funded networking projects. Since 2009, TYPES has been run as an
independent conference series. Previous TYPES meetings were held in
Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen (1993),
Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998),
Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002),
Torino (2003), Jouy en Josas near Paris (2004), Nottingham (2006),
Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw
(2010), Bergen (2011), Toulouse (2013), Paris (2014).

The TYPES areas of interest include, but are not limited to:

(Continue reading)

Luca Spada | 27 Feb 18:33 2015

TACL 2015 - Deadline extension for submissions

                 		School & Conference
 		            Call for extended abstracts
              School: 15 - 19 June 2015, University of Salerno (Italy)
              Conference: 21 - 26 June 2015, Ischia Island (Italy)


The deadline for submissions of abstracts has been extended to the 15th of March. 

Studying logics via semantics is a well-established and very active
branch of mathematical logic, with many applications, in computer
science and elsewhere. The area is characterised by results, tools and
techniques stemming from various fields, including universal algebra,
topology, category theory, order, and model theory. The programme of
the conference TACL 2015 will focus on three interconnecting
mathematical themes central to the semantic study of logics and their
applications: algebraic, categorical, and topological methods. This is
the seventh conference in the series Topology, Algebra, and Categories
in Logic (TACL). Earlier instalments of this conference have been
organised in Tbilisi (2003), Barcelona (2005), Oxford (2007),
Amsterdam (2009), Marseilles (2011), and Nashville (2013).
(Continue reading)

Jean-Pierre Marquis | 26 Feb 16:32 2015

A paper by MacLane

Does anyone have access to MacLane’s paper « Coherence and Canonical Maps », published in Symposia
Mathematica, vol. IV, Academic Press, London, pp. 231-242, 1970.

Please reply directly to me.



[For admin and other information see: ]

Marco Grandis | 26 Feb 09:29 2015

Preprint: Limits in multiple categories

There is now a second preprint in our series on multiple categories:

M. Grandis - R. Paré
Limits in multiple categories (On weak and lax multiple categories, II)
Pubbl. Mat. Univ. Genova, Preprint 605 (2015).

Abstract. Continuing our first paper in this series, we study  
multiple limits in infinite-dimensional multiple categories. The  
general setting is chiral multiple categories - a weak, partially lax  
form with directed interchanges.
After defining multiple limits we prove that all of them can be  
constructed from (multiple) products, equalisers and tabulators - all  
of them assumed to be respected by faces and degeneracies. Tabulators  
appear thus to be the basic higher limits, as was already the case  
for double categories.
Intercategories, a laxer form of multiple category already studied in  
two previous papers, are also considered. In this more general  
setting the basic multiple limits mentioned above can still be  
defined, but their general theory is not developed here.

The first paper of the series is:
M. Grandis - R. Paré
An introduction to multiple categories (On weak and lax multiple  
categories, I)
Pubbl. Mat. Univ. Genova, Preprint 604 (2015).

Marco Grandis and Bob Paré

(Continue reading)

Tarmo Uustalu | 25 Feb 20:12 2015

ETAPS 2016 call for satellite events

   19th European Joint Conferences on Theory and Practice of Software
                               ETAPS 2016
              Eindhoven, The Netherlands, April 2-8, 2016

                       Call for  Satellite Events


The European Joint Conferences on Theory and Practice of Software
(ETAPS) is the primary European forum for academic and industrial
researchers working on topics relating to Software Science. ETAPS is
an annual event which takes place in Europe each spring since 1998.

The nineteenth conference, ETAPS 2016, will take place April 2-8, 2016
in Eindhoven, The Netherlands.

ETAPS main conferences will take place on April 4-7, 2016. They are:

+ ESOP: European Symposium on Programming,
+ FASE: Fundamental Approaches to Software Engineering,
+ FOSSACS: Foundations of Software Science and Computation Structures,
+ POST: Principles of Security and Trust,
+ TACAS: Tools and Algorithms for the Construction and Analysis of


The ETAPS 2016 organizing committee invites proposals for satellite
events (workshops etc.) that will complement the main
(Continue reading)

Geoff Sutcliffe | 23 Feb 14:04 2015

LPAR-20 Call for Workshops

                  The 20th International Conference on
      Logic for Programming, Artificial Intelligence and Reasoning

              University of the South Pacific, Suva, Fiji

                           CALL FOR WORKSHOPS

LPAR-20 workshops will be held either as one-day or half-day events. If you
would like to propose a workshop for LPAR-20, please contact the workshop
chair via email (Peter.Baumgartner <at>, by the proposal deadline.

To help planning, workshop proposals should contain the following data:

- Name of the workshop.
- Brief description of the workshop, including workshop topics.
- Valid web address of the workshop.
- Contact information of the workshop organizers.
- An estimate of the audience size.
- Proposed format of the workshop (for example, regular talks, tool demos,
   poster presentations, etc.).
- Duration of the workshop (one-day or half-day).
- Potential invited speakers (if any).
- Procedures for selecting papers and participants.
- Special technical or AV needs.

Important dates
Workshop proposals submission deadline:     May 15, 2015
(Continue reading)

Zaganidis Dimitri | 23 Feb 11:17 2015

Young Topologists' Meeting 2015

Dear all,

This is the second and last annoucement for the Young Topologists' Meeting 2015 that will take place on July
6-10, 2015 at the EPFL in Lausanne, Switzerland.

The goal is to bring together graduate students, recent PhDs and young researchers to give talks
concerning their own work. In addition, there will be  two mini-courses:

Emily Riehl (Harvard University): Infinity category theory from scratch,
Gunnar Carlsson (Stanford University): Methods of applied topology.

The registration deadline is 30th April 2015. 
The deadline to apply for funding is 28th February 2015.

We can provide accommodation for about 70 participants.
Moreover, we applied for a NSF grant in order to fund about 20 participants  from American universities.
A full application, including recommendation letters and a CV, will be  requested upon positive answer
from the NSF.
We encourage women and under-represented minorities to apply.

The registration form and further information can be found on .

We hope to see you this summer in Switzerland!

The organizers,

Rachel Jeitziner,
Martina Rovelli,
Kay Werndli,
Dimitri Zaganidis.
(Continue reading)

Prof Robert Harper | 20 Feb 23:15 2015

OPLSS 2015

We are pleased to announce the preliminary program for the 14th annual  Oregon Programming Languages
Summer School (OPLSS) to be held June 15th to 27th, 2015 at the University of Oregon in Eugene.

This year's program is titled Types, Logic, Semantics, and Verification and features the following speakers:

Ahmal Ahmed
Northeastern University

Nick Benton
Microsoft Cambridge Research Lab

Adam Chlipala
Massachusetts Institute of Technology

Robert Constable
Cornell University

Peter Dybjer
Chalmers University of Technology

Robert Harper
Carnegie Mellon University

Ed Morehouse
Carnegie Mellon University

Greg Morrisett
Harvard University

Frank Pfenning
(Continue reading)

Neil Ghani | 20 Feb 19:02 2015

A HoTT-Date with Thorsten Altenkirch

Dear All

Dr Thorsten Altenkirch is visiting the MSP group during the week of March 2, and we thought we would have an
afternoon of talks in his honour on Wednesday 4 March. Please feel free to attend and forward this to anyone
else who might be interested. If you would like to give a talk, we could create a few spots too. Please get in
touch ASAP if you wish to i) attend; ii) give a talk; and/or iii) stay for dinner. This will help us to cater appropriately.

All the best
Neil and Fred

A HoTT-Date With Thorsten Altenkirch
(An Afternoon of Talks)

Date: Wednesday 4 March, 2pm
Location: Room 1415, Livingstone Tower, 26 Richmond Street, Glasgow G1 1XH.


Thorsten Altenkirch: Higher Inductive Types

Fredrik Nordvall Forsberg: Presentations of mutually defined types (including HITs)

James McKinna: Using relations to streamline the encode-decode method?

Neil Ghani: Higher Dimensional Parametricity via Cubical Categories

Bob Atkey: A Cubical Set Model for Relationally Parametric Type Theory

[For admin and other information see: ]
(Continue reading)

Lars Birkedal | 20 Feb 15:49 2015

Postdoc and PhD positions in Aarhus

Dear Colleagues,

We are looking for PhD students and postdocs in the area of
Programming, Logic and Semantics, here at Aarhus University, Denmark.
Several positions are available, in projects ranging from automated
static and dynamic analysis of libraries and frameworks for web
applications; theories and tools for language-based security; theories
and tools for modular reasoning about higher-order concurrent
imperative programs; and type theory and interactive proof assistants.

Please circulate this announcement to potential applicants and
encourage them to get in contact with one of us.

Best wishes,

Aslan Askarov (aslan <at><mailto:aslan <at>>)
Lars Birkedal (birkedal <at><mailto:birkedal <at>>)
Olivier Danvy (danvy <at><mailto:danvy <at>>)
Anders Møller (amoeller <at><mailto:amoeller <at>>)

Students interested in pursueing a PhD should apply
at the Graduate School for Science and Technology
(next deadline May 1, 2015).  They are encouraged to get
in contact with one of us before applying.

Potential postdocs should get in contact with us directly.
Positions are typically for 2 years.

(Continue reading)