[TYPES/announce] 29th WoLLIC 2023 - Call for Papers

[Ruy Jose Guerra Barretto de Queiroz]

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

[Please distribute. Apologies for multiple postings]

CALL FOR PAPERS

WoLLIC 2023
29th Workshop on Logic, Language, Information and Computation
11-14 July, 2023
Halifax, Nova Scotia, Canada

ORGANISATION
Department of Mathematics and Statistics, Dalhousie University, Canada
Centro de Informática, Universidade Federal de Pernambuco, Brazil

WoLLIC is an annual international forum on inter-disciplinary research
involving formal logic, computing and programming theory, and natural
language and reasoning. Each meeting includes invited talks and tutorials
as well as contributed papers. The twenty-ninth WoLLIC will be held at the
Department of Mathematics and Statistics, Dalhousie University, Halifax,
Nova Scotia, Canada, July 11 to 14, 2023. It is sponsored by the
Association for Symbolic Logic (ASL), the Interest Group in Pure and
Applied Logics (IGPL), the The Association for Logic, Language and
Information (FoLLI), the European Association for Theoretical Computer
Science (EATCS), and the Sociedade Brasileira de Lógica (SBL).

LOCATION
Halifax 
(https://urldefense.com/v3/__https://www.halifax.ca/__;!!IBzWLUs!TfQFH82-eSw7W43xC_ODUZ8bjcqqRYW74Ak1fr7HWrosrOfZ7fcYNw1xiR4rJShQbTmyR-23GpWnt-xFAGkszjTCll-o$
 ) is the capital and largest municipality
of the Canadian province of Nova Scotia, and the largest municipality in
Atlantic Canada. (Wikipedia)

FORMAT
WoLLIC 2023 will be a hybrid event.

SCOPE
Contributions are invited on all pertinent subjects, with particular
interest in cross-disciplinary topics. Typical but not exclusive areas of
interest are: foundations of computing, programming and Artificial
Intelligence (AI); novel computation models and paradigms; broad notions of
proof and belief; proof mining, type theory, effective learnability and
explainable AI; formal methods in software and hardware development;
logical approach to natural language and reasoning; logics of programs,
actions and resources; foundational aspects of information organization,
search, flow, sharing, and protection; foundations of mathematics;
philosophical logic; philosophy of language.

PAPER SUBMISSION
Proposed contributions should be in English, and consist of a scholarly
exposition accessible to the non-specialist, including motivation,
background, and comparison with related works. Articles should be written
in the LaTeX format of LNCS by Springer (see author's instructions at
https://urldefense.com/v3/__http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0__;!!IBzWLUs!TfQFH82-eSw7W43xC_ODUZ8bjcqqRYW74Ak1fr7HWrosrOfZ7fcYNw1xiR4rJShQbTmyR-23GpWnt-xFAGkszi72mchf$
 ). They must
not exceed 12 pages, with up to 5 additional pages for references and
technical appendices. The paper's main results must not be published or
submitted for publication in refereed venues, including journals and other
scientific meetings. It is expected that each accepted paper be presented
at the meeting by one of its authors either in person or via remote
connection. (At least one author is required to pay a full, on-site
registration fee before granting that the paper will be published in the
proceedings.) Papers must be submitted electronically at the WoLLIC 2023
EasyChair website 
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=wollic2023__;!!IBzWLUs!TfQFH82-eSw7W43xC_ODUZ8bjcqqRYW74Ak1fr7HWrosrOfZ7fcYNw1xiR4rJShQbTmyR-23GpWnt-xFAGkszvBIZ2l6$
 .

PROCEEDINGS
The proceedings of WoLLIC 2023, including both invited and contributed
papers, will be published in advance of the meeting as a volume in
Springer's LNCS series. In addition, abstracts will be published in the
Conference Report section of the Logic Journal of the IGPL, and selected
contributions will be published (after a new round of reviewing) as a
special post-conference WoLLIC 2023 issue of a scientific journal (tba).

INVITED SPEAKERS
(TBA)

STUDENT GRANTS
ASL sponsorship of WoLLIC 2023 will permit ASL student members to apply for
a modest travel grant (deadline: 90 days before the event starts). See
https://urldefense.com/v3/__http://www.aslonline.org/studenttravelawards.html__;!!IBzWLUs!TfQFH82-eSw7W43xC_ODUZ8bjcqqRYW74Ak1fr7HWrosrOfZ7fcYNw1xiR4rJShQbTmyR-23GpWnt-xFAGkszk9_2zWb$
  for details.

IMPORTANT DATES
February 20, 2023:  Abstracts deadline
February 27, 2023:  Full papers deadline
May 15, 2023: Author notification
June 5, 2023: Final version deadline  (firm)

PROGRAMME COMMITTEE
Bahareh Afshari (University of Amsterdam, Netherlands)
Zena Ariola (University of Oregon, USA)
Adriana Balan (University Politechnica of Bucharest, Romania)
Marta Bílková (Czech Academy of Sciences,  Czech Republic)
Josée Desharnais (Laval University, Canada)
David Fernández-Duque (Czech Academy of Sciences, Czech Republic)
Santiago Figueira (Universidad de Buenos Aires, Argentina)
Silvia Ghilezan (University of Novi Sad & Mathematical Institute SASA,
Serbia)
Sujata Ghosh 

[TYPES/announce] Call for Papers: NASA Formal Methods (NFM) 2023

[Rozier, Kristin-Yvonne [AER E]]

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

*
  The Fifteenth NASA Formal Methods Symposium

https://urldefense.com/v3/__https://conf.researchr.org/home/nfm-2023__;!!IBzWLUs!TNwWDVGGjF5GKWPzLkg1kPtWoG8XbHzoEwK1GcdcpBBaZP5zeJYQK9QR_kD2xbkX6f0XVWinRMMge4dgmcWC2OM56Ay0Ck6ZXzM$
 

    16 - 18 May 2023
University of Houston Clear Lake, Houston, Texas, USA
*


Theme of the Symposium:
---
The widespread use and increasing complexity of mission-critical and 
safety-critical systems at NASA and in the aerospace industry require 
advanced techniques that address these systems' specification, design, 
verification, validation, and certification requirements. The NASA 
Formal Methods Symposium (NFM) is an annual forum to foster 
collaboration between theoreticians and practitioners from NASA, 
academia, and industry. NFM's goals are to identify challenges and to 
provide solutions for achieving assurance for such critical systems.

New developments and emerging applications like autonomous software for 
uncrewed deep space human habitats, caretaker robotics, Unmanned Aerial 
Systems (UAS), UAS Traffic Management (UTM), and the need for 
system-wide fault detection, diagnosis, and prognostics provide new 
challenges for system specification, development, and verification 
approaches. The focus of these symposiums are on formal techniques and 
other approaches for software assurance, including their theory, current 
capabilities and limitations, as well as their potential application to 
aerospace, robotics, and other NASA-relevant safety-critical systems 
during all stages of the software life-cycle.

Topics of Interest:
---
We encourage submissions on cross-cutting approaches that bring together 
formal methods and techniques from other domains such as probabilistic 
reasoning, machine learning, control theory, robotics, and quantum 
computing among others.
     * Formal verification, including theorem proving, model checking, 
and static analysis
     * Advances in automated theorem proving including SAT and SMT solving
     * Use of formal methods in software and system testing
     * Run-time verification
     * Techniques and algorithms for scaling formal methods, such as 
abstraction and symbolic methods, compositional techniques, as well as 
parallel and/or distributed techniques
     * Code generation from formally verified models
     * Safety cases and system safety
     * Formal approaches to fault tolerance
     * Theoretical advances and empirical evaluations of formal methods 
techniques for safety-critical systems, including hybrid and embedded 
systems
     * Formal methods in systems engineering and model-based development
     * Correct-by-design controller synthesis
     * Formal assurance methods to handle adaptive systems


Important Dates:

Abstract Submission:  9 Dec 2022
Paper Submission:    16 Dec 2022
Paper Notifications: 20 Feb 2023
Camera-ready Papers: 12 Mar 2023
Symposium:    16-18 May 2023


Location & Cost:

The symposium will take place in the STEM Building at University of 
Houston Clear Lake, Houston, Texas, USA, 16-18 May 2023.

There will be no registration fee for participants. All interested 
individuals, including non-US citizens, are welcome to attend, to listen 
to the talks, and to participate in discussions; however, all attendees 
must register.


Submission Details:
---
There are two categories of submissions:

    1. Regular papers describing fully developed work and complete 
results (15 pages + references)
    2. Two categories of short papers: (6 pages + references)
    (a) Tool Papers describing novel, publicly-available tools
    (b) Case Studies detailing complete applications of formal methods 
to real systems with publicly-available artifacts

All papers should be in English and describe original work that has not 
been published or submitted elsewhere. All submissions will be fully 
reviewed by members of the Programme Committee. Papers will appear in 
the Formal Methods subline of Springer's Lecture Notes in Computer 
Science (LNCS) and must use LNCS style formatting 
(https://urldefense.com/v3/__https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines__;!!IBzWLUs!TNwWDVGGjF5GKWPzLkg1kPtWoG8XbHzoEwK1GcdcpBBaZP5zeJYQK9QR_kD2xbkX6f0XVWinRMMge4dgmcWC2OM56Ay0gHg_8X4$
 ). 
Papers must be submitted in PDF format at the EasyChair submission site:

https://urldefense.com/v3/__https://easychair.org/conferences/?conf=nfm2023__;!!IBzWLUs!TNwWDVGGjF5GKWPzLkg1kPtWoG8XbHzoEwK1GcdcpBBaZP5zeJYQK9QR_kD2xbkX6f0XVWinRMMge4dgmcWC2OM56Ay05Yjshho$
 


Keynote Speakers:
-
Julia Badger, NASA Johnson Space Center
Ken McMillan, UT Austin
Sanjit Seshia, UC Berkeley

[TYPES/announce] PhD Position in Theory

[Georg Moser]

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

4-year PhD position @ University of Innsbruck
==

Within the TCS Group of the Department of Computer Science at the 
University of Innsbruck, Austria there is an opening for a 4 year PhD 
student position; kindly see


https://urldefense.com/v3/__https://tcs-informatik.uibk.ac.at/vacancies/__;!!IBzWLUs!XgKY1begv1OxjvUnRvg9E0mEdD8ewx_6EG2VfQGwjZ-1M7HrhrCN4lw1uUZahx-WECReIIEqrKdvkDluDZ1R4wcJAM1qycC22Zz3Gt0$ 


for further details.

Applications (including CV, short letter of motivation, three 
references) should submitted via the following link


https://urldefense.com/v3/__https://lfuonline.uibk.ac.at/public/karriereportal.details?asg_id_in=13052__;!!IBzWLUs!XgKY1begv1OxjvUnRvg9E0mEdD8ewx_6EG2VfQGwjZ-1M7HrhrCN4lw1uUZahx-WECReIIEqrKdvkDluDZ1R4wcJAM1qycC26CTJH3c$ 

no later than December 22, 2022. Informal inquiries may be sent to 
georg.mo...@uibk.ac.at.


The city of Innsbruck is superbly located in the beautiful surroundings 
of the Tyrolean Alps. The combination of urban life in this historic 
town and the Alpine environment provides a high quality of living.


Further information is available from the following links:

- Theoretical Computer Science Group
  https://urldefense.com/v3/__https://tcs-informatik.uibk.ac.at/__;!!IBzWLUs!XgKY1begv1OxjvUnRvg9E0mEdD8ewx_6EG2VfQGwjZ-1M7HrhrCN4lw1uUZahx-WECReIIEqrKdvkDluDZ1R4wcJAM1qycC23MM95mE$ 
- Department of Computer Science
  https://urldefense.com/v3/__https://www.uibk.ac.at/informatik/__;!!IBzWLUs!XgKY1begv1OxjvUnRvg9E0mEdD8ewx_6EG2VfQGwjZ-1M7HrhrCN4lw1uUZahx-WECReIIEqrKdvkDluDZ1R4wcJAM1qycC2K8SPOrE$ 
- University of Innsbruck
  https://urldefense.com/v3/__https://www.uibk.ac.at/__;!!IBzWLUs!XgKY1begv1OxjvUnRvg9E0mEdD8ewx_6EG2VfQGwjZ-1M7HrhrCN4lw1uUZahx-WECReIIEqrKdvkDluDZ1R4wcJAM1qycC2jOiYuI8$ 


Best wishes,
Georg

---
Univ.-Prof. Dr. Georg Moser
Theoretical Computer Science, University of Innsbruck
Technikerstrasse 21a, 6020 Innsbruck

[TYPES/announce] Postdoc position in verification and automata learning at MPI-SWS, in association with Cornell and Oxford

[James Worrell]

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

A postdoctoral position in automated verification and automata learning is
open at the Max Planck Institute for Software Systems in Saarbrücken,
Germany, in the group of Prof. Joël Ouaknine. The project is a joint
collaboration with Prof. Alexandra Silva (Cornell University) and Prof.
James Worrell (Oxford University). The post is based in Saabrücken, but the
successful candidate will have the opportunity occasionally to travel to
Cornell (Ithaca, USA) and Oxford (UK).

Active automata learning has become an important technique in model-based
verification, as it enables the automated inference of models. There is a
gap between the existing learning algorithms and the expressive models that
have been used in e.g. probabilistic model checking. The goal of this
project is two-fold: on the one hand, we want to design active learning
algorithms for probabilistic automata and study the limits of learnability;
on the other hand, we want to explore their use in practical scenarios,
including randomised routing.

Qualifications:

-- A PhD awarded (or nearing completion) in Computer Science, Mathematics,
or a closely related discipline.

-- Knowledge and publications across some areas of: logic in computer
science, formal verification, automata theory, programming language theory,
probabilistic systems, learning, randomised algorithms, concurrency theory,
program synthesis.

This position is available on a full time basis for one year in the first
instance, with the possibility of renewal(s).

For informal enquiries, please contact Prof. Joël Ouaknine .

[TYPES/announce] COORDINATION 2023 Call For Papers

[emilio . tuosto]

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

25th International Conference on Coordination Models and Languages
June 19-23, 2023; Lisboa, Portugal

Website: 
https://urldefense.com/v3/__https://www.discotec.org/2023/coordination__;!!IBzWLUs!VWHrZyDPKRRhgp_HKV0U8WRsKxd71INDTXLY5ub6GALP3EbnUgOSaZHPSLyHpRPtr5oEGvrmXFPoZlH7C9KKSdd24qd8TmKf_g0NrA$
 

COORDINATION 2023 is one of the three conferences of DisCoTec 2023
https://urldefense.com/v3/__https://www.discotec.org/2023/__;!!IBzWLUs!VWHrZyDPKRRhgp_HKV0U8WRsKxd71INDTXLY5ub6GALP3EbnUgOSaZHPSLyHpRPtr5oEGvrmXFPoZlH7C9KKSdd24qd8TmITAYmKKA$
 

Submission Link: 
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=coordination2023__;!!IBzWLUs!VWHrZyDPKRRhgp_HKV0U8WRsKxd71INDTXLY5ub6GALP3EbnUgOSaZHPSLyHpRPtr5oEGvrmXFPoZlH7C9KKSdd24qd8TmITcjWrBg$
 
-


Call for Papers
---
Modern information systems rely increasingly on combining concurrent,
distributed,
mobile, adaptive, reconfigurable and heterogeneous components. New models,
architectures, languages and verification techniques are necessary to cope with
the complexity induced by the demands of today’s software development.
Coordination languages have emerged as a successful approach, in that
they provide
abstractions that cleanly separate behaviour from communication, therefore
increasing modularity, simplifying reasoning, and ultimately enhancing software
development. Building on the success of the previous editions, this conference
provides a well-established forum for the growing community of researchers
interested in models, languages, architectures, and implementation
techniques for
coordination.

Topics:
---
  * Theoretical models and foundations for coordination:
  component composition, concurrency, mobility, dynamic, spatial and
  probabilistic aspects of coordination, logic, emergent behaviour, types,
  semantics;
  * Specification, refinement, and analysis of architectures:
  patterns and styles, verification of functional and non-functional
  properties, including performance and security aspects;
  * Dynamic software architectures:
  distributed mobile code, configuration, reconfiguration, networked
  computing, parallel, high-performance and cloud computing
  * Nature- and bio-inspired approaches to coordination;
  * Coordination of multi-agent and collective systems:
  models, languages, infrastructures, self-adaptation, self-organisation,
  distributed solving, collective intelligence and emerging behaviour;
  * Coordination and modern distributed computing:
  web services, peer-to-peer networks, grid computing, context-awareness,
  ubiquitous computing, mobile computing;
  * Coordination platforms for infrastructures of emergent new
application domains
like IoT, fog- and edge-computing;
  * Cybersecurity aspects of coordinated systems, coordinated approaches to
cybersecurity;
  * Programming methodologies, languages, middleware, tools, and environments
for the development and verification of coordinated applications;
  * Tools, languages and methodologies for secure coordination;
  * Industrial relevance of coordination and software architectures:
  programming in the large, domain-specific software architectures and
  coordination models, case studies;
  * Interdisciplinary aspects of coordination;
  * Industry-led efforts in coordination and case studies.

We invite you to submit:
---
* Regular long papers (7-15 pages, not counting references):
describing thorough and complete research results and experience reports.
* Regular short papers (4-6 pages, not counting references):
describing research in progress or opinion papers on the past of
COORDINATION
research, on the current state of the art, or on prospects for the years to
come.
* Short tool papers (4-6 pages, not counting references):
describing technological artefacts in the scope of the research topics of
COORDINATION. Short tool papers are not required to provide an account of
theoretical foundations and are not required to present the design and
implementation concerns. They should provide a clear account of the tool’s
functionality and discuss the tool’s practical capabilities. The paper must
contain a link to a publicly downloadable MPEG-4 demo video of at most 10
minutes length.
* Long tool papers (7-15 pages, not counting references):
describing technological artefacts in the scope of the research topics of
COORDINATION. A full-length tool paper should provide a brief account of the
theoretical foundations (including relevant citations), present
the design and
implementation concerns (possibly including software architecture and core
data structures), provide a clear account of the tool’s
functionality, discuss

[TYPES/announce] 10 PhD studentships in Nottingham

[Graham Hutton]

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

Dear all,

The School of Computer Science at the University of Nottingham
in the UK is seeking applications for 10 fully-funded PhD
studentships: 
https://urldefense.com/v3/__https://tinyurl.com/ten-phd-2022__;!!IBzWLUs!VBm1bcV5i-SSEKb-M7KExGpuck3ljbNmp0m8XUx8pH2IB0ETEKNjVOvkPrCy5LbDnlP6MwzQVGCuYqUqgP0cEcv4K8QBvClVwXUcdTty_RFyQg$
 

Applicants in the area of the Functional Programming Lab
(tinyurl.com/fp-notts) are strongly encouraged!  If you are
interested in applying, please contact a potential supervisor
as soon as possible; the application deadline is 12th Feb 2023:

  Thorsten Altenkirch - constructive logic, proof assistants,
  homotopy type theory, category theory, lambda calculus.

  Ulrik Buchholtz - homotopy type theory, synthetic homotopy theory,
  proof assistants, constructive mathematics, and related topics.

  Graham Hutton - functional programming, haskell, category
  theory, program verification, program calculation.

  Nicolai Kraus - homotopy type theory, higher category theory,
  constructive mathematics, and related topics.

  Dan Marsden - category theory, logic, finite model theory,
  diagrammatic reasoning, foundations of computer science.

These positions are open to students of any nationality.

Best wishes,

The FP Lab

+---+

 10 Fully-Funded PhD Studentships

School of Computer Science
   University of Nottingham, UK

 
https://urldefense.com/v3/__https://tinyurl.com/ten-phd-2022__;!!IBzWLUs!VBm1bcV5i-SSEKb-M7KExGpuck3ljbNmp0m8XUx8pH2IB0ETEKNjVOvkPrCy5LbDnlP6MwzQVGCuYqUqgP0cEcv4K8QBvClVwXUcdTty_RFyQg$
 

Applications are invited from international and home students
for 10 fully-funded PhD studentships offered by the School of
Computer Science, starting on 1st October 2023.

The topics for the studentships are open, but should relate
to the interests of one the School's research groups:
Computational Optimisation and Learning; Computer Vision;
Cyber Security; Functional Programming; Intelligent Modelling
and Analysis; Mixed Reality; Uncertainty in Data and Decision
Making; Visualisation and Computer Graphics; Cyber-Physical
Health and Assistive Robotics Technologies.

The studentships are fully funded for 3.5 years and include a
stipend of £17,668 per year and tuition fees.  Applicants are
normally expected to have a first-class class bachelors or
masters in Computer Science or another relevant area, and
must obtain the support of a potential supervisor in the
School prior to submitting their application.

If you are interested in applying, please contact a potential
supervisor as soon as possible, and at least two weeks prior
to the closing date.  If the supervisor wishes to support
your application, they will direct you to make an official
application through the MyNottingham system.

Closing date for applications: Sunday 12th February 2023.

+---+


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

[TYPES/announce] ETH Zürich looking to hire assistant professor for "Software Security and Formal Methods" (deadline Jan 8)

[Ralf Jung]

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

Hi all,

ETH Zürich is looking to hire a tenure track assistant professor in "Computer 
Security", which includes "Software Security and Formal Methods".
From my own experience of being here for a grand total of not even 3 weeks, I 
can say that ETH is an a amazing place to work at, and Zürich is a great city. :D


For more information, see 
.

Also feel free to contact me with any questions.

Kind regards,
Ralf

[TYPES/announce] nominations for the Dahl-Nygaard prize for the 2023 year

[Davide Ancona]

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


  Dahl-Nygaard Prizes 2023: call for nominations 
[https://urldefense.com/v3/__https://sites.google.com/aito.org/home/aito-dahl-nygaard__;!!IBzWLUs!T5chiMebAS2ghCZ78k9Fn6suHim2cmnUAiMnYdRlWvK1xl6YhXTzcWsdBAAVauE7ZGEI2yBULyJAsonoy9w713vPmfZKCyWvoU_n1mw$ ]



In 2004, AITO established an annual prize in the name of the Ole-Johan Dahl and Kristen Nygaard to 
honor their pioneering work on object-orientation. The prizes are named after Ole-Johan Dahl and 
Kristen Nygaard, whose pioneering conceptual and technical work in the sixties shaped that view of 
programming and modeling which is now known as object-orientation.



One prize is awarded to a junior researcher (who has obtained the PhD degree at most 7 years before 
the award year, excluding any parental leave), and one prize to a senior researcher. The senior 
researcher should have made a significant long-term contribution to the field in research or 
engineering. The junior researcher should have made a promising contribution to the field through a 
paper, a thesis, or a prototype implementation.



Nominations are due by *December 15* and should be made using the following online form: 
https://urldefense.com/v3/__https://docs.google.com/forms/d/e/1FAIpQLSd9qQb8MmtkWM01vLhIpqPTIlmgciNwDiiLtSxot05x6k6c4w/viewform__;!!IBzWLUs!T5chiMebAS2ghCZ78k9Fn6suHim2cmnUAiMnYdRlWvK1xl6YhXTzcWsdBAAVauE7ZGEI2yBULyJAsonoy9w713vPmfZKCyWvGIeFcE4$ 


Davide Ancona (AITO Secretary) on behalf of John Boyland (Dahl-Nygaard prize 
committee chair, 2023)