From 7-11 January next year there will be a workshop on the Lean proof assistant at the Free University in Amsterdam.

The workshop will include introductory tutorials, scientific talks, and collaboration time for developers and users. Tutorials will be aimed at a mathematically experienced audience with little background in formal methods. Presentation topics may include (but are not limited to) the development of formal theories and libraries, tools and automation for formalization, the use of proof assistants in mathematics and computer science education, translating between formal and informal mathematics, and theoretical aspects of proof assistants. We welcome relevant work in proof assistants other than Lean. Participants who are interested in giving a talk or running a tutorial or discussion are asked to contact the organizers

From 7-11 January next year there will be a workshop on the Lean proof assistant at the Free University in Amsterdam.

The workshop will include introductory tutorials, scientific talks, and collaboration time for developers and users. Tutorials will be aimed at a mathematically experienced audience with little background in formal methods. Presentation topics may include (but are not limited to) the development of formal theories and libraries, tools and automation for formalization, the use of proof assistants in mathematics and computer science education, translating between formal and informal mathematics, and theoretical aspects of proof assistants. We welcome relevant work in proof assistants other than Lean. Participants who are interested in giving a talk or running a tutorial or discussion are asked to contact the organizers

From 7-11 January next year there will be a workshop on the Lean proof assistant at the Free University in Amsterdam.

The workshop will include introductory tutorials, scientific talks, and collaboration time for developers and users. Tutorials will be aimed at a mathematically experienced audience with little background in formal methods. Presentation topics may include (but are not limited to) the development of formal theories and libraries, tools and automation for formalization, the use of proof assistants in mathematics and computer science education, translating between formal and informal mathematics, and theoretical aspects of proof assistants. We welcome relevant work in proof assistants other than Lean. Participants who are interested in giving a talk or running a tutorial or discussion are asked to contact the organizers

From 7-11 January next year there will be a workshop on the Lean proof assistant at the Free University in Amsterdam.

The workshop will include introductory tutorials, scientific talks, and collaboration time for developers and users. Tutorials will be aimed at a mathematically experienced audience with little background in formal methods. Presentation topics may include (but are not limited to) the development of formal theories and libraries, tools and automation for formalization, the use of proof assistants in mathematics and computer science education, translating between formal and informal mathematics, and theoretical aspects of proof assistants. We welcome relevant work in proof assistants other than Lean. Participants who are interested in giving a talk or running a tutorial or discussion are asked to contact the organizers

From 7-11 January next year there will be a workshop on the Lean proof assistant at the Free University in Amsterdam.

The workshop will include introductory tutorials, scientific talks, and collaboration time for developers and users. Tutorials will be aimed at a mathematically experienced audience with little background in formal methods. Presentation topics may include (but are not limited to) the development of formal theories and libraries, tools and automation for formalization, the use of proof assistants in mathematics and computer science education, translating between formal and informal mathematics, and theoretical aspects of proof assistants. We welcome relevant work in proof assistants other than Lean. Participants who are interested in giving a talk or running a tutorial or discussion are asked to contact the organizers

The ILLC Colloquium is a half-yearly festive event (either the New Year's Colloquium, the Midsummernight Colloquium or the Midwinter Colloquium) that brings together the three research groups at the ILLC. Each colloquium consists of three main talks by representatives from the Logic and Language group, the Language and Computation group and the Logic and Computation group, which are occasionally followed by Wild Idea Talks. The colloquium is concluded by a get together of the entire ILLC community.

We are planning a meeting to discuss ICT facilities available to people at ILLC. In particular, we would like to make an inventory of
what is available now and to whom. And we wish to discuss if this is
enough, or if more is needed. And if so, what exactly.

Speakers: Kristof Bosmans, Bettina Klaus, Flip Klijn, Jordi Massó, Ton Storcken.

Substructural logics are formal reasoning systems that refine classical logic by weakening structural rules in a Gentzen-style sequent calculus. Traditionally, substructural logics have been investigated using proof theoretic and algebraic methods. In recent years, combined approaches have started to emerge. The programme of the SYSMICS conference will focus on interactions between syntactic and semantic methods in substructural logics. This conference is the last of a series of meetings planned in the SYSMICS RISE project during 2016-2019.

Substructural logics are formal reasoning systems that refine classical logic by weakening structural rules in a Gentzen-style sequent calculus. Traditionally, substructural logics have been investigated using proof theoretic and algebraic methods. In recent years, combined approaches have started to emerge. The programme of the SYSMICS conference will focus on interactions between syntactic and semantic methods in substructural logics. This conference is the last of a series of meetings planned in the SYSMICS RISE project during 2016-2019.

Substructural logics are formal reasoning systems that refine classical logic by weakening structural rules in a Gentzen-style sequent calculus. Traditionally, substructural logics have been investigated using proof theoretic and algebraic methods. In recent years, combined approaches have started to emerge. The programme of the SYSMICS conference will focus on interactions between syntactic and semantic methods in substructural logics. This conference is the last of a series of meetings planned in the SYSMICS RISE project during 2016-2019.

Substructural logics are formal reasoning systems that refine classical logic by weakening structural rules in a Gentzen-style sequent calculus. Traditionally, substructural logics have been investigated using proof theoretic and algebraic methods. In recent years, combined approaches have started to emerge. The programme of the SYSMICS conference will focus on interactions between syntactic and semantic methods in substructural logics. This conference is the last of a series of meetings planned in the SYSMICS RISE project during 2016-2019.

Substructural logics are formal reasoning systems that refine classical logic by weakening structural rules in a Gentzen-style sequent calculus. Traditionally, substructural logics have been investigated using proof theoretic and algebraic methods. In recent years, combined approaches have started to emerge. The programme of the SYSMICS conference will focus on interactions between syntactic and semantic methods in substructural logics. This conference is the last of a series of meetings planned in the SYSMICS RISE project during 2016-2019.

Shared mental models in the context of Explainable AI

Explainable AI is receiving a lot of attention these days. This is fantastic and important given the increasing use and impact of artificial intelligence, in particular Machine Learning. I think I have been working on Explainable AI for many years now, and I have always approached this from a Knowledge Representation point of view in which Shared Mental Models (and Team Mental Models) have played a big role. I would like to discuss this with you and come to some joint insights as to their possible roles in Explainable Machine Learning.

CWI organizes a meeting concerning Open Access aimed for a broad audience. It will be devoted to a discussion of Plan S, an initiative for Open Access publishing, launched in September 2018, and supported by an international consortium of research funders, including NWO, and to two radical initiatives, SciPost, and Open Research Central.