[TYPES/announce] JFP paper: POPLMark reloaded: Mechanizing proofs by logical relations

[Brigitte Pientka]

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

Dear all,

we would like to announce our recent JFP paper

POPLMark reloaded: Mechanizing proofs by logical relations
Andreas Abel, Guillame Allais, Aliya Hameer, Alberto Momigliano, Brigitte 
Pientka, Steven Schaefer, Kathrin Stark, Journal of Functional Programming, 29, 
E19. doi:10.1017/S0956796819000170

on how to mechanize proofs using logical relations on well-typed terms. It is 
an expanded version of B. Pientka's invited talk at Certified Proofs and 
Programs (CPP'19): POPLMark reloaded: Mechanizing proofs by logical relations.

Specifically, this paper provides a modern tutorial to proving strong 
normalization of a simply-typed lambda-calculus with a proof by  Kripke-style 
logical relations. Using this case study, we share some of the lessons learned 
tackling this problem in different dependently-typed proof environments. In 
particular, we consider the   mechanization in Beluga, a proof environment that 
supports higher-order abstract syntax encodings and contrast it to the 
development and strategies used in general purpose proof assistants such as Coq 
and Agda.

The goal of this paper is provide one benchmark to better understand, compare 
and push the state of the art of proof assistants and to engage the community 
in discussions on what support in proof environments is  needed to provide 
better support for modelling variable binding, contexts, renamings, 
substitutions, etc. 
 
We hope that other developers of proof assistants, graduate students, 
researchers, etc. feel inspired to mechanize this challenge problem, so we can 
better learn about the trade-offs between different systems/mechanization 
approaches.

All solutions to the problem (including solutions in F* and Lean) can be found 
at

https://poplmark-reloaded.github.io/


Best,

Andreas Abel,
Guillame Allais,
Aliya Hameer,
Alberto Momigliano,
Brigitte Pientka,
Steven Schäfer,
Kathrin Stark

[TYPES/announce] BCTCS & AlgoUK 2020 Final announcement and call for contributed talks

[Berger U.]

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

Final Announcement and call for contributed talks:

 * * * NOTE: We expect to be able to fund all (UK-based) researchers and PhD 
students. * * *

BCTCS & AlgoUK 2020
BRITISH COLLOQUIUM FOR THEORETICAL COMPUTER SCIENCE
6th - 8th April 2020, SWANSEA

http://www.cs.swan.ac.uk/bctcs2020

The 36th British Colloquium for Theoretical Computer Science will take place in 
Swansea from the afternoon of Monday 6 April to Wednesday 8 April 2020.

The purpose of BCTCS is to provide a forum in which researchers in theoretical 
computer science can meet, present research findings, and discuss developments 
in the field. It also aims to provide an environment in which PhD students can 
gain experience in presenting their work, and benefit from contact with 
established researchers.

The scope of the colloquium includes all aspects of theoretical computer 
science, including automata theory, algorithms, complexity theory, semantics, 
formal methods, concurrency, game theory, types, languages and logics.

BCTCS 2020 is being held together with the Fourth AlgoUK workshop which 
includes a session on Verification of Railway Control Systems. There will also 
be a special evening public forum on Formal Methods in Software Engineering.

The list of Invited Speakers includes

  Simon Chadwick - Siemens Rail Automation UK
  Robert Constable - Cornell University
  Edith Elkind - Oxford University
  Cliff Jones - University of Newcastle
  Bas Luttik - University of Eindhoven
  David Manlove - University of Glasgow
  Jan Peleska - Bremen University
  MS Ramanujan - Warwick University
  Patrick Totzke - University of Liverpool
  Helen Treharne - University of Surrey
  John Tucker - Swansea University
  Kristina Vuskovic - University of Leeds


SUBMISSION OF PRESENTATIONS

Participants wishing to give a 30 minute contributed talk on any topic within 
the scope of the colloquium are invited to submit a title and abstract via the 
BCTCS'2020 webpage. Presentations from research students and early career 
researchers are particularly encouraged. The titles and abstracts of all 
invited and contributed talks will appear in the Bulletin of the EATCS.

REGISTRATION AND BURSARIES

Registration information is available at the BCTCS'2020 webpage.

We have a number of bursaries worth £200 which can be used to reimburse the 
travel and accommodation expenses of UK-based researchers and PhD students. We 
hope to be able to offer these to all participants who provide a talk; but in 
the case of over-subscription, they will be allocated on a first-come, 
first-served basis. Hence, do propose a talk early.

IMPORTANT DATES (DEADLINES)

Talk proposals and Registration: 1 March 2020
Meeting: 6-8 April 2020


SPONSORS

BCTCS
AlgoUK
London Mathematical Society
Technocamps
Institute of Coding in Wales
Sony Technology Centre

---

BCTCS & AlgoUK 2020 Organizing Committee:
Ulrich Berger, Phillip James, Faron Moller, Liam O'Reilly, Filipos Pantekis, 
Olga Petrovska, Markus Roggenbach, Monika Seisenberger (Swansea University); 
and Daniel Paulusma, Iain Stewart (Durham University)
Copyright © 2020 BCTCS, All rights reserved.

[TYPES/announce] DEADLINE EXTENSION - Joint Call for Papers - DisCoTec2020

[Kiko Fernandez Reyes]

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

 [Apologies if you got multiple copies of this email.]



The abstract submission deadline has been extended to February 17.
The paper submission deadline has been extended to February 28.




   Joint Call for Papers

   15th International Federated Conference on
   Distributed Computing Techniques

   DisCoTec 2020

   Valletta, Malta, 15-19 June 2020

   https://www.discotec.org/2020



DisCoTec 2020 is one of the major events sponsored by the International
Federation for Information Processing (IFIP). It gathers conferences and
workshops that cover a broad spectrum of distributed computing subjects,
ranging from theoretical foundations and formal description techniques
to systems research issues.


* Main Conferences *

  - COORDINATION (https://www.discotec.org/2020/coordination)
22st IFIP International Conference on Coordination Models and
Languages
PC Chairs: Simon Bliudze (Inria Lille – Nord Europe, France) and
Laura Bocchi
(University of Kent, UK)

  - DAIS (https://www.discotec.org/2020/dais)
20th IFIP International Conference on Distributed Applications
and Interoperable Systems
PC Chairs: Anne Remke (University of Münster, Germany) and
Valerio Schiavoni (University of Neuchâtel, Switzerland)

  - FORTE (https://www.discotec.org/2020/forte)
40th IFIP International Conference on Formal Techniques for
Distributed Objects, Components and Systems
PC Chairs: Alexey Gotsman (IMDEA Software Institute, Spain)
and Ana Sokolova (University of Salzburg, Austria)


* Important Dates (for all main conferences) *

  - February 17, 2020: Submission of abstract -- extended
  - February 28, 2020: Submission of papers -- extended
  - April 10, 2020: Notification of accepted papers
  - April 24, 2020:  Camera ready
  - June 15-19, 2020: Conferences and Workshops


* Keynote Speakers *

- Nathalie Bertrand, INRIA Rennes Bretagne-Atlantique
- Holger Hermanns, Saarland University
- Ken McMillan, Microsoft Research, Redmond
- Peter Kriens, OSGi Alliance


* Submission Categories *

COORDINATION:
Full papers (up to 15 pages + 2 pages references),
Short papers (up to 6 pages + 2 pages references),
Survey papers (up to 25 pages + 2 pages references),
Tool papers (up to 6 pages + 2 pages references + 10min demo video).

DAIS
Full papers (up to 15 pages + 2 pages references).
Full practical experience reports (up to 15 pages + 2 pages references)
Work-in-progress (up to 6 pages + 2 pages references)

FORTE
Full papers (page limit: up to 15 pages + 2 pages references)
Short papers (page limit: up to 6 pages + 2 pages references)
(Rough diamonds, Tool (demonstration) papers, Position papers)
“Journal First” papers (page limit: up to 2 pages, including references)
More information is available on the conference website.


* Proceedings *

The proceedings of DisCoTec 2020 main conferences will be published in
Springer's LNCS-IFIP volumes.


* Special issue *

The individual conferences will organise special issues of extended and
selected papers in reputable journals such as Logical Methods in
Computer Science and Journal of Parallel and Distributed Computing.

More information is available at the conference website.


* Submission Instructions *

Authors are invited to submit their contributions electronically in PDF
using a two-phase online submission process. Registration of the paper
information and abstract (max. 250 words) must be completed before
February 3, 2020. Submission of the manuscript is due no later than
February 14, 2020. Submissions are handled through the EasyChair
conference management system:
  https://easychair.org/conferences/?conf=coordination2020
  https://easychair.org/conferences/?conf=dais2020
  https://easychair.org/conferences/?conf=forte20

Contributions must be written in English and report on original,
unpublished work not submitted for publication elsewhere (cf. IFIP's
Author Code of Conduct, see http://www.ifip.org/ under
Publications/Links). The submissions must not exceed the total page
number limit, including figures and references, prepared using
Springer’s LNCS style. Submissions not adhering to the above specified
constraints may be rejected without review.

DisCoTec conferences welcome contributions in theoretical models and
foundations of coordination, concurrency, programming languages,
practical and conceptual aspects of distributed computations as well as
models and formal specification, testing and verification methods for
distributed computing.

Detailed information about the topics, the submission categories and the
corresponding page limits are available at the conference website.

For each accepted paper, one of the authors must register to DisCoTec
2020 and attend the 

[TYPES/announce] CfP: SCSS 2020

[Temur Kutsia]

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

=
SCSS 2020
The 9th International Symposium on Symbolic Computation in Software Science
  -- In the era of Computational and Artificial Intelligence  --

September 10-13, 2020, Gammarth, Tunisia
https://scss2020.doodlekit.com/
=

Overview

Symbolic Computation is the science of computing with symbolic objects
(terms, formulae, programs, representations of algebraic objects etc.).
Powerful algorithms have been developed during the past decades for the
major subareas of symbolic computation: computer algebra and
computational logic. These algorithms and methods are successfully
applied in various fields, including software science, which covers a
broad range of topics about software construction and analysis.

Meanwhile, artificial intelligence methods and machine learning
algorithms are widely used nowadays in various domains and, in
particular, combined with symbolic computation. Several approaches mix
artificial intelligence and symbolic methods and tools deployed over
large corpora to create what is known as cognitive systems. Cognitive
computing focuses on building systems which interact with humans
naturally by reasoning, aiming at learning at scale.

The purpose of SCSS 2020 is to promote research on theoretical and
practical aspects of symbolic computation in software science, combined
with modern artificial intelligence techniques.


Scope
--
SCSS 2020 solicits submissions on all aspects of symbolic computation
and their applications in software science, in combination with
artificial intelligence and cognitive computing techniques. The topics
of the symposium include, but are not limited to the following:

- automated reasoning, knowledge reasoning, common-sense reasoning and
reasoning in science
- algorithm (program) synthesis and/or verification, alignment and joint
processing of formal, semi-formal, and informal libraries.
- formal methods for the analysis of network and system security
- termination analysis and complexity analysis of algorithms (programs)
- extraction of specifications from algorithms (programs)
- theorem proving methods and techniques, collaboration between
automated and interactive theorem proving
- proof carrying code
- generation of inductive assertion for algorithm (programs)
- algorithm (program) transformations
- combinations of linguistic/learning-based and semantic/reasoning methods
- formalization and computerization of knowledge (maths, medicine,
economy, etc.)
- methods for large-scale computer understanding of mathematics and science
- artificial intelligence, machine learning and big-data methods in
theorem proving and mathematics
- formal verification of artificial intelligence and machine learning
algorithms, explainable artificial intelligence, symbolic artificial
intelligence
- cognitive computing, cognitive vision, perception systems and
artificial reasoners for robotics
- component-based programming
- computational origami
- query languages (in particular for XML documents)
- semantic web and cloud computing


Important Dates
---
Title and abstract due: May 8, 2020
Manuscript due: May 15, 2020
Author notification: July 6, 2020
Early registration: July 31, 2020
Camera ready papers: August 10, 2020
Conference dates: September 10-13, 2020


Invited Speakers
--
Tateaki Sasaki (University of Tsukuba, Japan)
Jean-Pierre Jouannaud (Ecole Normale Superieure de Paris-Saclay, France)


General Chairs
-
Adel Bouhoula (Sup'Com, Carthage University, Tunisia)
Tetsuo Ida (Tsukuba University, Japan)


Program Chair
-
Temur Kutsia (Johannes Kepler University, Austria)


Program Committee
-
Hassan Ait-Kaci (HAK Language Technologies)
Changbo Chen (Chinese Academy of Sciences, China)
Rachid Echahed (CNRS, Grenoble, France)
Seyed Hossein Haeri (UC Louvain, Belgium)
Mohamed-Bécha Kaâniche (Sup’Com, Carthage University, Tunisia)
Cezary Kaliszyk (University of Innsbruck, Austria)
Yukiyoshi Kameyama (University of Tsukuba, Japan)
Michael Kohlhase (University of Erlangen–Nuremberg, Germany)
Laura Kovacs (Vienna University of Technology, Austria)
Temur Kutsia (Johannes Kepler University, Austria) Chair
Zied Lachiri (ENIT, University of Tunis El Manar, Tunisia)
Christopher Lynch (Clarkson University, USA)
Yasuhiko Minamide (Tokyo Institute of Technology, Japan)
Yoshihiro Mizoguchi (Kyushu University, Japan)
Julien Narboux (Strasbourg University, France)
Michaël Rusinowitch (INRIA, France)
Sofiane Tahar (Concordia University, Canada)
Mateu Villaret (University of Girona, Spain)
Dongming Wang (CNRS, Paris, France)


Local Organization Committee

Mohamed-Bécha Kaâniche (Sup’Com, Carthage University, Tunisia) (Chair)
Faouzi Jaidi (ESPRIT University, Tunisia) (Website Admin)
Tarek Abbess (Sfax University, Tunisia)
Takoua Kefi (Kairouan University, Tunisia)
Aida 

[TYPES/announce] FSCD 2020 - Extended deadline (Abstract: February 10/ Submission: February 13)

[Sandra Alves]

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

(Apologies for multiple copies of this announcement. Please circulate.) 

==
Updated information on: Abstract and Submission dates
==

CALL FOR PAPERS
Fifth International Conference on
   Formal Structures for Computation and Deduction (FSCD 2020)
 June 29 – July 5, 2020, Paris, France
   http://fscd2020.org/ 
 
IMPORTANT DATES
---
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not 
be considered.
   Abstract: February 10, 2020 *** extended  
   Submission:February 13, 2020 *** extended  
   Rebuttal: March 28-29, 2020  
   Notification: April 13, 2020 
   Final version:  April 27, 2020  

INVITED SPEAKERS

- René Thiemann:  FSCD-IJCAR joint speaker
  (http://cl-informatik.uibk.ac.at/users/thiemann/ 
)
- John Harrison: FSCD-IJCAR joint speaker
  (https://www.cl.cam.ac.uk/~jrh13/ ) 
- Brigitte Pienta
  (https://www.cs.mcgill.ca/~bpientka/ )
- Andrew Pitts
  (https://www.cl.cam.ac.uk/~amp12/ )
- Simona Ronchi della Rocca
  (http://www.di.unito.it/~ronchi/ )   

FSCD (http://fscdconference.org/  ) covers all 
aspects of formal structures for computation 
and deduction from theoretical foundations to applications. Building on two 
communities, RTA
(Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and 
Applications), 
FSCD embraces their core topics and broadens their scope to closely related 
areas in logics, 
models of computation, semantics and verification in new challenging areas. 

The suggested, but not exclusive, list of topics for submission is:

1. Calculi: Rewriting systems (string, term, higher-order, graph, conditional, 
modulo, infinitary, etc.);
Lambda calculus; Logics (first-order, higher-order, equational, modal, 
linear, classical, constructive, etc.); 
Proof theory (natural deduction, sequent calculus, proof nets, etc.); Type 
theory and logical frameworks; 
Homotopy type theory; Quantum calculi.

2. Methods in Computation and Deduction: Type systems (poly- morphism, 
dependent, recursive, intersection, session, etc.); 
Induction, coinduction; Matching, unification, completion, order- ings; 
Strategies (normalization, completeness, etc.); 
Tree automata; Model building and model checking; Proof search and theorem 
proving; 
Constraint solving and decision procedures.

3. Semantics: Operational semantics and abstract machines; Game Semantics and 
applications; 
Domain theory and categorical models; Quantitative models (timing, 
probabilities, etc.); 
Quantum computation and emerging models in computation.

4. Algorithmic Analysis and Transformations of Formal Systems: Type Inference 
and type checking; 
Abstract Interpretation; Complexity analysis and implicit computational 
complexity; 
Checking termination, confluence, derivational complexity and related 
properties; Symbolic computation.

5. Tools and Applications: Programming and proof environments; Verification 
tools;
Proof assistants and interactive theorem provers; Applications in industry; 
Applications of formal sys- tems in other sciences.

6. Semantics and Verification in new challenging areas: Certification; 
Security; Blockchain protocols; 
Data Bases; Deep learning and machine learning algorithms; Planning.

PUBLICATION

The proceedings will be published as an electronic volume in the Leibniz 
International
Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl. All LIPIcs proceedings 
are open access.

SPECIAL ISSUE
--
Authors of selected papers will be invited to submit an extended version to a 
special issue of 
Logical Methods in Computer Science.

SUBMISSION GUIDELINES 
--
Submissions can be made in two categories. Regular research papers are limited 
to 15 pages, 
excluding references. They must present original research which is unpublished 
and not submitted elsewhere. 
Proofs and other technical details that do not fit within the page limit can be 
submitted as an appendix (up to 5 pages). 
The appendix will be consulted at the discretion of the reviewers. Therefore, 
submissions must be self-contained within 
the respective page limit; the additional material should not be necessary to 
assess the merits of a submission. 
System descriptions are limited to 15 pages, excluding 

[TYPES/announce] Caleidoscope Complexity School: Call for Participation

[Thomas Seiller]

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

*** Call for participation ***

Caleidoscope: Research School in Computational Complexity

Paris, 15-19 June 2020

http://caleidoscope20.sciencesconf.org/ 




Dear all,

We are delighted to announce the second edition of the Caleidoscope Research 
School in Computational Complexity, to take place in Paris, 15-19 June 2020. 
The school is aimed at graduate students and researchers who already work in 
some aspects of computational complexity and/or who would like to learn about 
the various approaches.



DESCRIPTION

Computational complexity theory was born more than 50 years ago when 
researchers started asking themselves what could be computed efficiently. 
Classifying problems/functions with respect to the amount of resources (e.g. 
time and/or space) needed to solve/compute them turned out to be an extremely 
difficult question. This has led researchers to develop a remarkable variety of 
approaches, employing different mathematical methods and theories.

The future development of complexity theory will require a subtle understanding 
of the similarities, differences and limitations of the many current 
approaches. In fact, even though these study the same phenomenon, they are 
developed today within disjoint communities, with little or no communication 
between them (algorithms, logic, programming theory, algebra...). This 
dispersion is unfortunate since it hinders the development of hybrid methods 
and more generally the advancement of computational complexity as a whole.

The goal (and peculiarity) of the Caleidoscope school is to reunite in a single 
event as many different takes on computational complexity as can reasonably be 
fit in one week.  It is intended for graduate students as well as established 
researchers who wish to learn more about neighbouring areas.



LECTURES

1. Algorithms and lower bounds. Lecturer: Ryan Williams, MIT.
2. Hardness of Approximation. Lecturer: Luca Trevisan, Bocconi University.
3. Higher-Order Complexity. Lecturer: Bruce Kapron, University of Victoria.
4. Parametrized Complexity. Lecturer: Daniel Marx, Max Planck Institute 
Saarbrucken.

In addition to these broad-ranging themes, there will also be three tutorials 
on more focussed topics.

5. Quantum Computation and Complexity. Lecturer: Elham Kashefi, CNRS and 
Sorbonne University.
6. Static Complexity Analysis. Lecturer: Georg Moser, University of Innsbruck.
7. Complexity Theory for Black-Box Optimization Heuristics. Lecturer: Carola 
Doerr, CNRS and Sorbonne University.



REGISTRATION

Registration to the school is free but mandatory. This is to help us plan 
tea/coffee breaks and social activities.

https://caleidoscope20.sciencesconf.org/registration/ 




FINANCIAL SUPPORT

There may be opportunities for financial support for participants. We will make 
relevant information available via the webpage.
https://caleidoscope20.sciencesconf.org/ 




ORGANISERS
Damiano Mazza — CNRS & Université Sorbonne Paris Nord
Sylvain Perifel — Université Paris 7
Thomas Seiller — CNRS & Université Sorbonne Paris Nord



SPONSORS

European Mathematical Society (EMS)
DIM RFSI - Région Île-de-France (https://dim-rfsi.fr/)
CNRS (https://www.cnrs.fr/en)
Université Sorbonne Paris Nord (https://www.univ-paris13.fr/en/)
Laboratoire d'Informatique de Paris Nord (https://lipn.univ-paris13.fr/)
Université Paris 7 (https://www.univ-paris-diderot.fr)
Institut de Recherche en Informatique Fondamentale 
(https://www.irif.fr/en/index)



signature.asc
Description: Message signed with OpenPGP

[TYPES/announce] Senior Postdoc / Project Coordinator position in Information Security and Program Verification at ETH Zurich

[Mueller Peter]

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

Senior Postdoc / Project Coordinator position in Information Security and 
Program Verification at ETH Zurich

The Institute of Information Security (the groups of Prof. Adrian Perrig and 
Prof. David Basin) and the Programming Methodology Group (Prof. Peter Müller) 
at ETH Zurich are hiring a Postdoc in a large research project in the area of 
digital trust. The goal of this project is to develop a comprehensive, formally 
verified security architecture for communication in the physical and digital 
world. In particular, the project will develop protocols to transfer physical 
trust relationships into the digital world and store, manage, and use them. The 
design will take into account human (mis-)behavior from the outset. A 
particular emphasis is on the formal verification of the architecture both at 
the design and implementation level to rule out any undesired behavior.

We are looking for enthusiastic and outstanding postdoctoral researchers with a 
strong background in some of the following topics:

  *   formal modeling and verification,
  *   program verification,
  *   theorem proving, model checking,
  *   cryptographic protocols,
  *   public-key infrastructure, identity management, authentication,
  *   networking and distributed systems, and
  *   design and implementation of security architectures.

In addition to research, the responsibilities of the position include project 
management, in particular, coordination among the involved research groups, 
lightweight reporting to the funding agency, and outreach to potential 
industrial users of the developed solutions.

All candidates matching the profile above are encouraged to apply as soon as 
possible. We will process applications until all positions are filled. 
Successful candidates are expected to start soon after acceptance, but the 
starting date is negotiable.

Applications should include:

  *   a curriculum vitae,
  *   a brief description of research interests, and
  *   letters of recommendation.

Applications and inquiries should be sent to Christoph Sprenger and Sandra 
Schneider at the following email addresses.

  infsec.positi...@inf.ethz.ch, 
jobs...@inf.ethz.ch
Postdocs are paid employees of ETH Zurich. Salary and employment conditions are 
attractive. Zurich is a diverse and multicultural city which is consistently 
rated among the best cities in the world in which to live.