[TYPES/announce] Reminder: PhD positions in Stockholm, deadline this Friday, 22 April

[Peter LeFanu Lumsdaine]

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

Dear all,

A reminder for all interested in the PhD openings here that the deadline is
*this Friday*, 22 April (full information repeated below).

(Note: if you’ve contacted me about this before last week and I haven’t
replied yet, please write again — at least a couple of inquiries got caught
in my spam filter, so it’s possible there are more I missed, for which my
apologies!  If you wrote last week, expect a reply today.)

Best,
–Peter.


Dear all,

We are recruiting for PhD students in HoTT (and other topics) at the
Stockholm University Department of Mathematics, starting Autumn 2022.  The
deadline for applications is Friday, April 22.

Full details and application are through the university website:
https://urldefense.com/v3/__https://www.su.se/english/about-the-university/work-at-su/available-jobs/phd-student-positions-1.507588?rmpage=job=17395=UK__;!!IBzWLUs!AZmFWVrBxolcx8HvniMCF972CP4GIijk4IINObI2NvehuDX_mwjTAXw2mAnrjQ33ChKB54K_PRAYJA$
 
  Please contact me if you have any questions about the position!  And (for
advisors) please pass this on to any interested masters-level students.

Answers to a few common questions:
- PhD positions in Sweden are fully funded, with a livable salary.
- The position includes up to 20% teaching.
- Swedish speaking isn’t required, either formally or practically (though
learning it during the PhD is encouraged) — all higher-level teaching is
done in English, and most administrative business (including all
necessities) can be.

Best wishes,
–Peter.

[TYPES/announce] BX 2022 - Call for papers (deadline 14 May)

[Li-yao Xia]

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

# Tenth International Workshop on Bidirectional Transformations (BX 2022)

8 July 2022, Nantes, France
Part of STAF 2022 (5-8 July): https://urldefense.com/v3/__https://staf2022.univ-nantes.io/__;!!IBzWLUs!HVmu13GoSx6nR257McO-uEqVxxvUQz9MShWvlUD3i3m2rkQLGVw2j8YCOP_KxdB-gnD55j7ERyMcUw$ 

BX 2022 homepage: https://urldefense.com/v3/__http://bx-community.wikidot.com/bx2022:home__;!!IBzWLUs!HVmu13GoSx6nR257McO-uEqVxxvUQz9MShWvlUD3i3m2rkQLGVw2j8YCOP_KxdB-gnD55j7MWunzRA$ 




## Overview

Bidirectional transformations (BX) are a mechanism for maintaining the
consistency between two or more related (and heterogeneous) sources of
information (e.g., relational databases, software models and code, or
any other artefacts following standard or domain-specific formats). The
strongest argument in favour of BX is its ability to provide a
synchronization mechanism that is guaranteed to be correct by
construction. BX has been attracting a wide range of research areas and
communities, with prominent presence at top conferences in several
different fields (namely databases, programming languages, software
engineering, and graph transformation). Nowadays, the fast-growing
complexity of software- or data-intensive systems has forced industry
and academia to use and investigate different development techniques to
manage the many different aspects of the systems. Researchers are
actively investigating the use of bidirectional approaches to tackle a
diverse set of challenges with various applications including
model-driven software development, visualization with direct
manipulation, big data, databases, domain-specific languages,
serializers, and data transformation, integration and exchange. BX 2022
is a dedicated venue for BX in all relevant fields and is part of a
workshop series that was created in order to promote cross-disciplinary
research and awareness in the area. As such, since its beginning in
2012, the workshop has rotated between venues in different fields.

Papers for BX 2022 can be submitted on EasyChair:
https://urldefense.com/v3/__https://www.easychair.org/conferences/?conf=bx2022__;!!IBzWLUs!HVmu13GoSx6nR257McO-uEqVxxvUQz9MShWvlUD3i3m2rkQLGVw2j8YCOP_KxdB-gnD55j4RbEIZUA$ 




## Important Dates

- Paper submission: 14 May, 2022
- Author notification: 28 May, 2022
- Workshop: 8 July, 2022



## Topics

The aim of the workshop is to bring together researchers and
practitioners, established and new, interested in bx from different
perspectives, including but not limited to:

- bidirectional programming languages and frameworks
- software development with BX
- data and model synchronization
- view updating
- inter-model consistency analysis and repair
- data/schema (or model/metamodel) co-evolution
- coupled software/model transformations
- inversion of transformations and data exchange mappings
- domain-specific languages for BX
- analysis and classification of requirements for BX
- bridging the gap between formal concepts and application scenarios
- analysis of efficiency of transformation algorithms and benchmarks
- model-driven and model-based approaches
- survey and comparison of BX technologies
- case studies and tool support
- applications and experiences of adopting BX in the real world



## Categories of Submissions

Five categories of submissions are considered:

1. Full Research Papers (13-15 pages) - in-depth presentations of novel
concepts and results - applications of bx to new domains - survey papers
providing novel comparisons between existing bx technologies and
approaches, case studies

2. Tool Papers (7-8 pages) - guideline papers presenting best practices
for employing a specific bx approach (with a specific tool) -
presentation of new tools or substantial improvements to existing ones -
qualitative and/or quantitative comparisons of applying different bx
approaches and tools

3. Experience Report (7-8 pages) - sharing experiences and lessons
learned with bx tools/frameworks/languages - how bx is used in
(research/industrial/educational) projects

4. Short Papers (5 pages) - work in progress - small focused
contributions - position papers and research perspectives - critical
questions and challenges for bx

5. Talk Proposals (2 pages) - proposed lectures about topics of interest
for bx - existing work representing relevant contributions for bx -
promising contributions that are not mature enough to be proposed as
papers of the other categories



## Submission guidelines

Papers should use the new CEUR-ART style, single column, available as an
Overleaf page or as a zip archive:

https://urldefense.com/v3/__https://www.overleaf.com/read/gwhxnqcghhdt__;!!IBzWLUs!HVmu13GoSx6nR257McO-uEqVxxvUQz9MShWvlUD3i3m2rkQLGVw2j8YCOP_KxdB-gnD55j7IRZGwYw$ 

[TYPES/announce] Postdoc position in Tokyo: model checking and optimization metaheuristics

[Ichiro Hasuo]

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

[Please distribute, apologies for multiple postings.]

Open Position for a PostDoc Researcher
(Model Checking Extended with Optimization Metaheuristics, April 2022)

ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD
) invites applications for a postdoc
researcher. We aim to combine model checking and optimization
metaheuristics, in order to scale formal verification techniques up to
real-world industrial problems that are complex and black-box. We aim to do
so, at the same time, in a way guided by solid meta-theoretical foundations
such as those which we've presented in LICS and CAV. We thus explore new
shapes of application of logic to modern software and systems. The position
will be especially suited for those who have experience in model checking
research and who wish to expand their research portfolio.

Some further details are found below. See
https://urldefense.com/v3/__https://group-mmm.org/eratommsd/open-position-for-a-postdoc-researcher-march-2022/__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZntWM2LN3g$
 
for full details.

Thanks a lot for your consideration.
Best, Ichiro


-
JOB DESCRIPTION

The candidate will work at National Institute of Informatics
, Tokyo, Japan, and will pursue a novel
extension of model checking techniques (temporal logic, automata theory)
with optimization metaheuristics (evolutionary computation, stochastic
optimization, statistical machine learning).

The goal is to overcome two major challenges that currently limit the
applicability of formal verification techniques to real-world industrial
systems, namely *scalability* and the *absence of white-box models*. In our
endeavor towards the goal, we do not mind relying on testing, rather than
exhaustive verification; this puts us somewhat closer to so-called *lightweight
formal methods*.

That said, our theoretical development shall be nothing "lightweight." We
believe that there is a great theoretical depth here--we will explore the
depth using logical, automata-theoretic, and/or categorical machinery.
This *theory
of * *"lightweight" formal methods* will significantly expand the current
landscape of application of logic to software.

The position should be especially suited for model checking researchers who
wish to expand their research portfolio. We find case studies in our
industrial collaborations and seek applicability to those real-world
problems (they are mostly from the manufacturing industry). At the same
time, we seek rigorous logical/automata-theoretic/categorical foundations
for the solutions we come up with--so our work stays well in the realm of
the formal verification community. We work in an interdisciplinary
environment, and the candidate will be constantly exposed to interaction
with control theory, software engineering, automated driving, and category
theory.

The candidate will work closely with Prof. Ichiro Hasuo
 and a few other team members. It is
possible that the candidate be granted an academic title (such as Project
Assistant/Associate Professor).
References

The following are some outcomes of our efforts so far. They are listed here
in order to exemplify concrete topics. Note that the topics of these papers
are diverse, and the candidate is not expected to follow all of them. A
good match with one of them would suffice.

   - Masaki Waga, Étienne André, Ichiro Hasuo: Symbolic Monitoring Against
   Specifications Parametric in Time and Data. CAV (1) 2019: 520-539. doi
   
 arXiv
   

   (The topic is the theory of timed automata, which strikes a balance
   between theory and applicability.)
   - Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, Ichiro Hasuo: Widest
   Paths and Global Propagation in Bounded Value Iteration for Stochastic
   Games. CAV (2) 2020: 349-371 doi
   
 arXiv
   

[TYPES/announce] EXPRESS/SOS 2022 second call for Papers

[Claudio Mezzina]

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

===
SECOND CALL FOR PAPERS
Combined
29th International Workshop on Expressiveness in Concurrency
and
19th Workshop on Structural Operational Semantics
(EXPRESS/SOS 2022)

https://urldefense.com/v3/__https://express-sos2022.github.io/__;!!IBzWLUs!H0yVAJg1NU2rxZlb5Wu373ySCXCJdzivsv3m4foVfvGtluXzYylF4lQhJhmFnM3t8ML6ROGIE2AHbw$
 

Warsaw (Poland)
September 12, 2022, Affiliated with CONCUR 2022

Submission deadline (full and short papers):
Friday, July 1, 2022
===



== INVITED SPEAKERS

Silvia Crafa (University of Padova, Italy)
Ross Horne (University of Luxembourg, Luxembourg)



== SCOPE AND TOPICS
The EXPRESS/SOS workshop series aims at bringing together researchers
interested in the formal semantics of systems and programming
concepts, and in the expressiveness of computational models.

Topics of interest for EXPRESS/SOS 2022 include, but are not limited to:

- expressiveness and rigorous comparisons between models of
computation (process algebras, event structures, Petri nets, rewrite
systems)
- expressiveness and rigorous comparisons between programming
languages and models (distributed, component-based, object-oriented,
service-oriented);
- logics for concurrency (modal logics, probabilistic and stochastic
logics, temporal logics and resource logics);
- analysis techniques for concurrent systems;
- theory of structural operational semantics (meta-theory,
category-theoretic approaches, congruence results);
- comparisons between structural operational semantics and other
formal semantic approaches;
- applications and case studies of structural operational semantics;
- software tools that automate, or are based on, structural
operational semantics.

We especially welcome contributions bridging the gap between the above
topics and neighbouring areas, such as, for instance:
- computer security
- multi-agent systems
- programming languages
- formal verification
- reversible computation
- knowledge representation


== SUBMISSION GUIDELINES:
We invite two types of submissions:
* Full papers (up to 15 pages, excluding references).
* Short papers (up to 5 pages, excluding references, not included in
the workshop proceedings)

All submissions should adhere to the EPTCS format 
(https://urldefense.com/v3/__http://www.eptcs.org__;!!IBzWLUs!H0yVAJg1NU2rxZlb5Wu373ySCXCJdzivsv3m4foVfvGtluXzYylF4lQhJhmFnM3t8ML6ROGTF0pFNg$
 ).
Simultaneous submission to journals, conferences or other workshops is
only allowed for short papers; full papers must be unpublished.

Submission is performed through EasyChair:
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=expresssos2022__;!!IBzWLUs!H0yVAJg1NU2rxZlb5Wu373ySCXCJdzivsv3m4foVfvGtluXzYylF4lQhJhmFnM3t8ML6ROFj2Mko1Q$
 

The final versions of accepted full papers will be published in EPTCS.
It is understood that for each accepted submission one of the
co-authors will register for the workshop and give the talk.
We are monitoring the COVID-19 pandemic to decide if the workshop
will take place physically in Warsaw, online, or hybrid.
Whatever the decision, we will guarantee the possibility of online
participation.


== SPECIAL ISSUE
There is a long tradition of special issues of reputed international
journals devoted to the very best papers presented in prior editions
of the workshop.
We are planning a special issue with selected papers from EXPRESS/SOS 2021
and EXPRESS/SOS 2022.
More information will follow closer to the event.


== IMPORTANT DATES
- Paper submission: July 1, 2022
- Notification date: August 5, 2022
- Camera ready version: August 19, 2022
- Workshop: September 12, 2022


== WORKSHOP CO-CHAIRS:
Valentina Castiglioni (Reykjavik University, IS)
Claudio Antares Mezzina (University of Urbino, IT)


== PROGRAM COMMITTEE:
Georgiana Caltais (University of Konstanz, Germany)
Valentina Castiglioni (Reykjavik University, Iceland), co-chair
Wan Fokkink (Vrije University Amsterdam, The Netherlands)
Paola Giannini (University of Piemonte Orientale, Italy)
Daniel Hirschkoff (ENS Lyon, France)
Tobias Kappe (Cornell University, UK)
Vasileios Koutavas (Trinity College Dublin, Ireland)
Ondrej Lengal (Brno University of Technology, Czech Republic)
Gerald Luettgen (University of Bamberg, Germany)
Claudio Antares Mezzina (University of Urbino, Italy), co-chair
Max Tschaikowski (Aalborg University, Denmark)

== CONTACT
Prospective authors are encouraged to contact the co-chairs in case of
questions at express-so...@easychair.org