Jiri Adamek | 9 Oct 15:27 2015

terminology of (co)algebras

Does anyone know who was the first author to speak about F-algebras
and/or F-coalgebras where F is a mere endofunctor? Lambek proved his
famous lemma without using any name for the objects. And Arbib and Manes
proved a number of properties but used the word "F-dynamics".

Thanks Jiri

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Geoff Sutcliffe | 6 Oct 16:21 2015

IWIL-11 in Fiji, extended deadline

          11th International Workshop on the Implementation of Logics

                         FINAL CALL FOR PAPERS
                   Extended deadline: October 15, 2015.

The 11th International Workshop on the Implementation of Logics will be held in
November 2015 in conjunction with the 20th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning in Suva, Fiji

We are looking for contributions describing implementation techniques for and
implementations of automated reasoning programs, theorem provers for various
logics, logic programming systems, and related technologies. Topics of interest
include, but are not limited to:

+ Propositional logic and decision procedures, including SMT
+ First-order and higher order logics
+ Non-classical logics, including modal, temporal, description, non-monotonic reasoning
+ Formal foundations for efficient implementation of logic
+ Data structures and algorithms for the efficient representation and processing of logical concepts
+ Proof/model search organization and heuristics for logical reasoning systems
+ Data analysis and machine learning approaches to search control
+ Techniques for proof/model search visualization and analysis
+ Practical constraint handling
+ Reasoning with ontologies and other large theories
+ Implementation of efficient theorem provers and model finders for different logics
+ System descriptions of logical reasoning systems
+ Issues of reliability, witness generation, and  witness verification
+ Evaluation and benchmarking of provers and other logic-based systems
+ I/O standards and communication between reasoning systems

(Continue reading)

Venkata Rayudu Posina | 5 Oct 05:31 2015

Decision-making and Category theory

Dear All,

Would you be kind enough to point me to literature (papers / books) on
the applications of category theory to decision-making problems.

Thanking you,
Yours truly,

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Joost Vercruysse | 1 Oct 16:35 2015

Announcement conference Stef Caenepeel 60

Dear colleague,

In 2016, Stef Caenepeel will turn 60. To celebrate this joyful event, a conference is organized in Turin,
Italy, from Tue 24 - Fri 27 May 2016 entitled

"Brauer groups, Hopf algebras and monoidal categories.
-- A conference in honour of Stef Caenepeel on the occasion of his 60th birthday"

Hereby, you are cordially invited to participate in this meeting. A (tentative) list of speakers can be
found at the end of this message.

A poster session is organized for PhD students and young post-docs who would like to present their results
during the meeting.

The conference website can be found on the address:
If you are interested to attend the conference, please fill out the registration form that is available on
this site.
Feel free to forward this message to everyone who might be interested.

We hope to be welcoming you in Turin next May,

Best wishes,
The organizers,

Ana Agore
Alessandro Ardizzoni
Sorin Dascalescu
Isar Goyvaers
Gigel Militaru
(Continue reading)

Marcelo Fiore | 1 Oct 16:17 2015

Faculty position in PL/verification/theorem-proving at Cambridge.

Faculty position in PL/verification/theorem-proving at Cambridge
[this is roughly analogous to a US tenured associate professor position]

The University of Cambridge Computer Laboratory is seeking to recruit a
new faculty member at the Lecturer or Senior Lecturer level who can
contribute to research in areas such as (but not limited to) the

    - theoretical foundations of programming
    - programming language design and implementation
    - formal specification and verification of computer systems
    - theorem proving and its application to hardware and software

The ideal candidate will have interests that range from mathematical
theory to practical applications and will demonstrate the potential to
collaborate with Computer Laboratory research students, staff and faculty
across a range of topics.

Notwithstanding the above focus, exceptional candidates from any area of
Computer Science are also encouraged to apply.

It is likely that successful candidates will already have a strong track
record in one or more relevant research areas and already have some
postdoctoral experience. Ideally the candidate will also have experience
of teaching and generating research grant income.

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

(Continue reading)

Peter Selinger | 1 Oct 03:20 2015

type theory postdoc at Dalhousie University

Dear colleagues,

I invite applications for one postdoctoral position, starting between
now and January 1, at Dalhousie University under my supervision.

The successful applicant will work on a project entitled "Trusted
Quantum Software via a Formally Verified Functional Quantum
Programming Language". Specifically, the project will involve the
design of a type system for a type-safe functional programming
language for quantum computing, loosely modelled on the Quipper
language (http://www.mathstat.dal.ca/~selinger/quipper/). It will also
involve developing the meta-theory (including categorical semantics)
of the language, and eventually the formalization of some of this
meta-theory in a proof assistant.

Familiarity with type theory (especially dependent type theory),
programming language design, and/or semantics will be a prerequisite
for this postdoc. Familiarity with quantum computing will be helpful,
but is neither necessary nor sufficient for this position - the main
emphasis is on programming languages and type systems.

Although the position will be held at Dalhousie University in Canada,
it will be an asset if the candidate is able to travel, because I will
be spending one semester in Germany and one semester in the U.S. next
year, and ideally I would like the postdoc to be able to accompany me.

Funding for the project comes from the U.S. Air Force Office of
Scientific Research, and the research project will be part of a team
effort also involving collaborators from Tulane, Stanford, Oxford, the
University of Iowa, and the University of Pennsylvania.
(Continue reading)

Eduardo Ochs | 30 Sep 03:08 2015

Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children

Hi list,

I think (and hope) that the following seminar notes may be interesting
to some people...

   "Intuitionistic Logic for Children, or:
    Planar Heyting Algebras for Children"

Feedback VERY welcome!
Cheers =),
   Eduardo Ochs

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Benno van den Berg | 29 Sep 19:31 2015

Postdoc position at the ILLC

Dear all,

There is a three-year postdoc position available at the ILLC, which is part
of the University of Amsterdam. The deal is that applicants should also
submit a proposal for a VENI-grant with NWO, the Dutch Science
Organization, and should get a favorable review. This implies that only
people who are eligible for the VENI can apply, which for most applicants
means that they must have obtained their PhD in 2013, 2014 or 2015. The
deadline for the application for the postdoc position is 1 November 2015,
while the deadline for the VENI-application is 5 January 2016. More
information is available here:


If you have any questions, feel free to contact me.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Olivia Caramello | 28 Sep 19:45 2015

"Topos a l'IHES" - second announcement

Dear All,

We are pleased to announce the following international conference on topos
theory, which will take place at IHES from 23 to 27 November 2015.

Everyone is welcome.

Best regards,
Olivia Caramello (on behalf of the Organizing Committee) 

Call for participation

23-27 November 2015
Institut des Hautes Etudes Scientifiques 

* Scope *

The conference aims to illustrate the fruitfulness and wide-ranging 
impact of the theory of Grothendieck toposes, by featuring presentations on 
new theoretical advances in the subject (including the theory of higher
as well as on applications of toposes in different fields such as number
algebraic geometry, logic, functional analysis, topology, mathematical
(Continue reading)

Tarmo Uustalu | 28 Sep 12:03 2015

ETAPS 2016 final call for papers


                   CALL FOR PAPERS: ETAPS 2016

19th European Joint Conferences on Theory And Practice of Software

            Eindhoven, The Netherlands, 2-8 April 2016




ETAPS is the primary European forum for academic and industrial
researchers working on topics relating to software science. ETAPS,
established in 1998, is a confederation of five main annual
conferences, accompanied by satellite workshops. ETAPS 2016 is the
ninteenth event in the series.

-- MAIN CONFERENCES (4-7 April) --

    * ESOP: European Symposium on Programming
        (PC chair Peter Thiemann, Universit├Ąt Freiburg, Germany)
    * FASE: Fundamental Approaches to Software Engineering
        (PC chairs Perdita Stevens, University of Edinburgh, UK,
         and Andrzej Wasowski, IT University of Copenhagen, Denmark)
    * FOSSACS: Foundations of Software Science
        and Computation Structures
        (PC chairs Bart Jacobs, Radboud Universiteit Nijmegen, 
(Continue reading)

Michael Barr | 27 Sep 18:55 2015

Latest version of diagxy

I have just uploaded to CTAN the latest version of diagxy.  It is also 
available from my own web site: http://www.math.mcgill.ca/barr/papers/. 
The main thing it does is work well with the beamer macro \uncover (and 
relatives) to allow you use the node and arrow mode to add arrows (or for 
that matter, nodes) as overlays on diagrams.  It also solves a problem 
that one user reported to me that the registration on repeatedly laying 
down the same ink was not perfect and he claimed that his nodes were 
thickened.  I never observed this but the same fix apparently fixes it. 
Also, I have added \hyperref to the diaxydoc file.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]