[TYPES/announce] 5-year Postdoc fellowship in Computer Science (PL) for Climate Science at University of Cambridge

[Dominic Orchard]

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

More details and to apply: 
https://urldefense.com/v3/__https://www.jobs.cam.ac.uk/job/40147/__;!!IBzWLUs!Q6Wr_lGQtDRGhNs-aTw-xQ-11NOgCG2hvfJinTnifEcqp_wK8fUDB42gobv25yEdARLlGcA-W6GV_24e0nFTAX_5P4b4F8kvQ5s$
 
Closing date 31st May 2023

Computational modelling is at the core of climate science, where complex
models of earth systems are key to the scientific process. Most models
embed significant inherent and accidental complexity which hampers
verification and maintenance, reproducibility, and performance. There is
consequently a pressing need for computer science research to provide the
tools and techniques that climate scientists need to deliver new
high-quality, high-performance, and high-assurance models.

Applying the latest computer science research to support climate science is
the aim of this 5-year Early Career Academic Fellowship in the new
Institute of Computing for Climate Science (ICCS) at the University of
Cambridge. The institute is a joint venture between the Department of
Applied Mathematics and Theoretical Physics, the Department of Computer
Science and Technology and University Information Services, thanks to a
philanthropic donation from Schmidt Futures.

ICCS will improve understanding of our changing climate through the
development and dissemination of models for scientific computing. ICCS
hosts a team of Research Software Engineers who work directly with four
international Virtual Earth Systems Research Institutes (VESRI) to address
computation and research software needs of climate scientists. This
Fellowship offers a unique opportunity to carry out foundational research
into computational support for climate science, with access to climate
science teams.

As part of the interdisciplinary ICCS team, this opening is for an
outstanding research scientist with expertise in working across the
interfaces between data science, computer science and climate science. As
part of the University of Cambridge, ICCS has a significant education and
training component, through the commitment towards sharing its scientific
insights openly and broadly, and will contribute strongly to Cambridge
Zero, the University's climate change initiative, that is identifying
routes to the creation of a sustainable, zero-carbon future for all.

Areas of expertise that are welcomed for this fellowship include:

   -

   Parallelisation and high-performance computing.
   -

   Programming language design and implementation.
   -

   Data visualisation and analysis.
   -

   Verification, particularly for numerical computing.
   -

   Machine learning in the context of modelling and its effective
   programming

Fellows will be encouraged to develop their own research agenda, with
guidance and mentoring by the ICCS directors, in particular Dr Dominic
Orchard who leads the Computer Science vision of the institute, and with Dr
Jeremy Yallop.

The Fellow will be affiliated with the Department of Computer Science and
Technology and expected to collaborate with the Research Software Engineers
within ICCS and the VESRI Science teams. The appointment has generous
travel and research expenses support, and will allow Fellows to supervise
PhDs, apply for other funding, and engage with teaching within ICCS and
across the University. The position also includes dining rights at Queens'
College.

Role requirements:

   -

   A PhD in Computer Science or another relevant subject area.
   -

   Normally at least three years' research experience (obtained in either
   academic or industrial settings).
   -

   A strong track record of published research in one or more relevant
   areas.
   -

   Evidence of potential for interdisciplinary collaborations.
   -

   Evidence of potential to obtain additional research funding.

Experience of teaching and research supervision is desirable.

We will consider the possibility of appointing at a lower grade (i.e.
Research Associate, with salary range £33,348-£43,155, rather than Senior
Research Associate) in the case of an exceptional candidate with less than
3 years' experience post-PhD. Appointment at Senior Research Associate
level is dependent on significant experience as a research associate or
equivalent. In both cases, successful candidates will hold (or be close to
completing) a PhD. Appointment at research associate level is dependent on
having a PhD. Where a PhD has yet to be awarded, appointment will initially
be made as a research assistant and amended to research associate when the
PhD is awarded.

This is a fixed term appointment and funds are initially available for 5
years. If you have questions regarding the role or application process,
please contact Dominic Orchard (dominic.orch...@cl.cam.ac.uk) or Jeremy
Yallop (jeremy.yal...@cl.cam.ac.uk).

Please quote reference NR35996 on your application and in any
correspondence about this vacancy.

The University actively 

[TYPES/announce] Postdoc position in automata and concurrency theory at the University of Warsaw

[Sławomir Lasota]

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

We invite applications of motivated and research-focused individuals to
carry out research on mathematical models of concurrent systems as part
of the NCN project "Frontiers of automatic analysis of concurrent systems".
The project aims at advancing theoretical foundations at the borderline
between automata theory, concurrency and formal verification.

The successful candidate will be hosted by the automata theory group
at the University of Warsaw, offering:

- a vibrant working atmosphere,
- exciting and challenging research problems,
- competitive salary,
- collaborations worldwide.

**
- Application deadline: May 25, 2023
- Starting date: flexible
- Duration: one year, possible extension to another year
- Principal investigator: Slawomir Lasota  
(https://urldefense.com/v3/__http://www.mimuw.edu.pl/*sl__;fg!!IBzWLUs!S4XLjs3gkFcYkQ3PSrdNZaHGAp4ZtdvOy0saU95hcu5Y23A8l_anoTyRGRYHrXRj_2nqYyeOktcv08Hmc7VT-PQlTbKSPNWbYQ$
 )
- Contact: s...@mimuw.edu.pl
**

The ideal candidate is expected to have:

- PhD degree or equivalent in computer science or math
- solid background in formal methods or automata theory
- excellent publication record
- strong motivation for research work in foundations of computer science
- advanced skills in written and spoken English.

For details of application and recruitment procedure, please contact
Sławomir Lasota at s...@mimuw.edu.pl

[TYPES/announce] TYPES 23 - Call for Participation

[Eduardo Hermo Reyes]

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

CALL FOR PARTICIPATION

29th International Conference on Types for Proofs and Programs, TYPES 2023

12-17th June 2023, ETSInf, Universitat Politècnica de València, Spain

https://urldefense.com/v3/__https://types2023.webs.upv.es/__;!!IBzWLUs!QoV4DvLiS_9dyQ5O3iqgjDSgU3_1fZ1YBjXGFpyR9QQc9JkNTftM6vd3QRIOXyWI-Ee2WbQtP0QQlglb4LX2yh2bN4PBLZVqK2-Z$ 


Early registration deadline: **May, 21st 2023**
Registration: https://urldefense.com/v3/__https://types2023.webs.upv.es/Registration.html__;!!IBzWLUs!QoV4DvLiS_9dyQ5O3iqgjDSgU3_1fZ1YBjXGFpyR9QQc9JkNTftM6vd3QRIOXyWI-Ee2WbQtP0QQlglb4LX2yh2bN4PBLWYxQJB6$ 


INVITED SPEAKERS

Simona Ronchi della Rocca - Università di Torino
Marie Kerjean - CNRS
Andrej Bauer - University of Ljubljana
Yannick Foster - INRIA Nantes

PROGRAMME & ACCEPTED PAPERS

https://urldefense.com/v3/__https://types2023.webs.upv.es/Programme.html__;!!IBzWLUs!QoV4DvLiS_9dyQ5O3iqgjDSgU3_1fZ1YBjXGFpyR9QQc9JkNTftM6vd3QRIOXyWI-Ee2WbQtP0QQlglb4LX2yh2bN4PBLSooJP7t$ 


REGISTRATION FEES

To facilitate their attendance, TYPES'23 offers a reduced rate for
students, available in the registration form. In addition, all
registrations performed before May, 21st will be offered a discount.

BACKGROUND

The TYPES meetings are a forum to present new and on-going work in all
aspects of type theory and its applications, especially in formalised
and computer assisted reasoning and computer programming.

The TYPES areas of interest include, but are not limited to:

* foundations of type theory and constructive mathematics;
* applications of type theory;
* dependently typed programming;
* industrial uses of type theory technology;
* meta-theoretic studies of type systems;
* proof assistants and proof technology;
* automation in computer-assisted reasoning;
* links between type theory and functional programming;
* formalizing mathematics using type theory.

CONTACT

Email: types2023 AT upv.es

ORGANIZERS

Alicia Villanueva (VRAIN-UPV, Spain)
Mireia González Bedmar (Formal Vindications, Spain)

[TYPES/announce] Autumn school "Proof and Computation", Herrsching (Germany), 10-16 Sep 2023

[xu]

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

[Second call for participation. Apologies for the multiple postings.]

  Autumn school "Proof and Computation"
 Herrsching, Germany, 10th to 16th September 2023
  https://urldefense.com/v3/__http://www.mathematik.uni-muenchen.de/*schwicht/pc23.php__;fg!!IBzWLUs!TJtHdJho7PsqQZsbf0MZDI9cl7CeKnapF0y5CAWKY0etHT2SdgB56cg7PLQJP33aawyv8CzHxIagEls_O020V-AXp88$ 


This year's international autumn school "Proof and Computation" will be held
from 10th to 16th September 2023 in Herrsching near Munich. Its aim is  
to bring
together young researchers in the field of Foundations of Mathematics,  
Computer

Science and Philosophy.

SCOPE

- Predicative Foundations
- Constructive Mathematics and Type Theory
- Computation in Higher Types
- Extraction of Programs from Proofs

COURSES

- Stefania Centrone: Husserl on the Totality of all Conceivable  
Arithmetical Operations

- Yannik Forster: MetaCoq
- Hugo Herbelin: The logical structure and computational contents of  
choice, barinduction and related principles

- Matthias Hutzler: Introduction to synthetic algebraic geometry
- Georg Moser: Cichon's conjecture on the slow growing hierarchy
- Andrea Rechenberger: Philosophy and history of computation: Turing machine
- Monika Seisenberger: Extraction of programs from proofs

WORKING GROUPS

There will be an opportunity to form ad-hoc groups working on specific
projects, but also to discuss in more general terms the vision of
constructing correct programs from proofs.

APPLICATIONS

Graduate or PhD students and young postdoctoral researchers are invited to
apply.  Applications (e.g. a self-introduction including research interests
and motivation) should be sent to

Chuangjie Xu .

Students are required to provide also a letter of recommendation, preferably
from the thesis adviser.

Deadline for applications: **31st May 2023**.

Applicants will be notified by 28th June 2023.

FINANCIAL SUPPORT

Successful applicants will be offered **full-board accommodation** for
the days of the autumn school.  There are NO funds, however, to reimburse
travel or further expenses, which successful applicants will have to
cover otherwise.

The workshop is supported by the Udo Keller Stiftung (Hamburg), the
CID (Computing with Infinite Data) programme of the European Commission
and a JSPS core-to-core project.


Klaus Mainzer
Peter Schuster
Helmut Schwichtenberg

[TYPES/announce] TLLA 2023 : deadline extension

[Stefano Guerrini]

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

[Apologies if you receive multiple copies of this message]

Dear colleagues, 

the deadline for TLLA 2023 (7th International Workshop on Trends in Linear 
Logic and Applications) that will be held in Rome, 1-2 July colocated with FSCD 
has been extended. Here it is the new dates:

* Submission deadline:21 May 2023
* Notification to authors:26 May 2023 
* Final versions due: 7 June 2023 

Please, find below the new version of the call for paper, that you can also 
find on the site of the workshop


https://urldefense.com/v3/__https://tlla.linear-logic.org/2023__;!!IBzWLUs!RtFOF9PyIysIji9idrKS8ExktP8flYCBtzWWozVpLKpEU_kCPqlcX8-btsBP1yDqUiO_AzYnIpDSOIzpWTtdIr9MiK3cXrTTYeRbSO1DuYhaplO8FQ$
 

Best wishes

—sg

=

Stefano Guerrini
Professeur des Universités
Institut Galilée, Université Sorbonne Paris Nord (USPN)
Laboratoire d'Informatique de Paris-Nord (LIPN), CNRS (UMR 7030)
stefano.guerr...@univ-paris13.fr


==
   Call for Papers

  TLLA  2023

  7th International Workshop on
  Trends in Linear Logic and Applications

  Rome, 1-2 July 2023

 Affiliated with FSCD 2023


https://urldefense.com/v3/__https://tlla.linear-logic.org/2023/__;!!IBzWLUs!RtFOF9PyIysIji9idrKS8ExktP8flYCBtzWWozVpLKpEU_kCPqlcX8-btsBP1yDqUiO_AzYnIpDSOIzpWTtdIr9MiK3cXrTTYeRbSO1DuYhCn4X1cw$
 

==

Linear Logic is not only a proof theoretical tool to analyze or
control the use of resources in logic and computation. It is also a
corpus of tools, approaches, and methodologies (proof nets,
exponential decomposition, geometry of interaction, coherent spaces,
relational models, etc.) that, even if developed for studying Linear
Logic syntax and semantics, have been applied in several other fields
(analysis of lambda-calculus computations, game semantics, computational
complexity, program verification, etc.).

The TLLA international workshop aims at bringing together researchers
working on Linear Logic or applying it or its tools. The main goal is
to present and discuss trends in the research on Linear Logic and its
applications by means of tutorials, invited talks, open discussions,
and contributed talks.

The purpose is to gather researchers interested in the connections
between Linear Logic and various topics such as

* theory of programming languages
* games and languages
* proof theory
* categories and algebra
* implicit computational complexity
* parallelism and concurrency
* quantum and probabilistic computing
* models of computation
* possible connections with combinatorics
* functional analysis and operator algebras
* philosophy
* linguistics


--
** Submission Guidelines
--

Contributions are not restricted to talks presenting an original
results, but open to tutorials, open discussions, and position
papers. For this reason, we strongly encourage contributions
presenting work in progress, open questions, and research
projects. Contributions presenting the application of linear logic
results, techniques, or tools to other fields, or vice versa, are most
welcome.

To propose a contributed talk, send an email with the pdf file of a 
short abstract to

tll...@irif.fr 

Please specify in the email message the names of the corresponding
authors and their emails, if different from the sending one, which in any
case will be used for further communications. The abstract, whose length
should be between 2 and 5 page, must include the names and the email
addresses of all the authors. 

--
** Important dates
--

* Submission deadline:15 May 2023
* Notification to authors:22 May 2023 
* Final versions due: 31 May 2023 

* Workshop date:  1-2 July 2023

--
** Publication
--

The abstracts of the contributed and invited talks will be published
on the site of the conference.
Possible other formats will be discussed at the workshop.

--
** Tutorials
--

* Alexis Saurin, Université Paris Cité, France
* Zeinab Galal, Sorbonne Université, France

--
** Invited Speakers

[TYPES/announce] Assistant Professor in Computer Science at Chalmers University of Technology

[Ana Bove]

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

TheComputer Science and Engineering departmentat Chalmers University of 
Technology, Sweden,is currently seeking applications for the (tenure 
track) position of *Assistant Professor in Computer Science*.


The Computing Science Division 
 
is recruiting an Assistant Professor. The position is open to qualified 
applicants with research and teaching excellence in any area broadly 
covered by the Division, such as programming languages, cybersecurity 
and privacy, natural language processing, formal methods, logic, and 
type theory. Our research spans the whole spectrum of computer science, 
from theoretical foundations to application areas. We have extensive 
national and international collaboration with academia and industry all 
around the world.



The full details of the position, including the application procedure 
and deadline, can be found onourwebsite:


Assistant Professor Position in Computer Science 



Please do now hesitate to contact me or any of my colleagues if you have 
any questions regarding the position, the department or any other 
matter. We would be very happy to help you in any way we can!


Yours sincerely

--
-- Ana Bove, Docent
Phone: (46)(31) 772 1020
https://urldefense.com/v3/__http://www.cse.chalmers.se/*bove__;fg!!IBzWLUs!VWlhODSqCiXM9Og-QHO5rs74tInOarspSjww7rk3aG0Oc7TkuhJer9b0FyTl8wuKDMX-pEWqeOcyD-ocyyydurbczur6Aw$ 
Department of Computer Science and Engineering

Chalmers Univ. of Technology and Univ. of Gothenburg

[TYPES/announce] Three Lectureships in Computer Science at Sussex

[Bernhard Reus]

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

The School of Engineering and Informatics at the University of Sussex is 
appointing new academic staff in Computer Science as part of a strategy to grow 
and complement the current strengths in the Department of Informatics.

There are three new positions  -- "Lecturer in Computer Science“ -- created to 
work in the Department of Informatics. This position is equivalent to Assistant 
Professor.

The successful candidate will undertake research and teaching within the 
department. They will be associated with one of the research groups (Artificial 
Intelligence, Creative Technology, Foundations of Software Systems) and 
expected to teach at undergraduate and postgraduate levels.

Research in the "Foundations of Software Systems" group subsumes Type Theory, 
Logic, and Program Verification.

For more information please see:

https://urldefense.com/v3/__https://www.sussex.ac.uk/about/jobs/lecturer-in-computer-science-ref-20110-20111-20112__;!!IBzWLUs!VMhHsVRH_Aly-Rb5sw0PF3iv-t8k-yRWDyN0o__QWFuamZGS7zMYJIU18kzw-VLRIFd8gYfsaOvi8vRKJ4ME7le2Ai2LeGtWHpue$
 


Best,
 Bernhard

——
Dr Bernhard Reus
Head of Foundations of Software Systems
Department of Informatics
University of Sussex

[TYPES/announce] HoTT 2023 -- Programme and final registration

[Steve Awodey]

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

[Apologies for duplicate emails]

*** HoTT 2023
*** Second International Conference on Homotopy Type Theory
*** Carnegie Mellon University
*** 22nd-25th May 2023

The Programme is now available here:

https://urldefense.com/v3/__https://hott.github.io/HoTT-2023/*programme/__;Lw!!IBzWLUs!Xy148gZ5yzhDz8kV6sWBcRy07OUjbxnz_zih5M0rnAPTHYUxR5fAZcVh3MYOsR_cc4jZgitc0KBnZY1finnpZGItbXFNXMhWJ08$
 

Registration will close on 14 May. 
Until then you can still register via the website:

https://urldefense.com/v3/__https://hott.github.io/HoTT-2023/*registration/__;Lw!!IBzWLUs!Xy148gZ5yzhDz8kV6sWBcRy07OUjbxnz_zih5M0rnAPTHYUxR5fAZcVh3MYOsR_cc4jZgitc0KBnZY1finnpZGItbXFNTVtURI0$
 

With best regards,

Steve (on behalf of the Scientific and Organising Committees)

[TYPES/announce] FTfJP 2023 (co-located with ECOOP/ISSTA in Seattle) Call for Papers

[Summers, Alexander]

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

==
CALL FOR PAPERS
FTfJP 2023

25th Workshop on Formal Techniques for Java-like Programs
July 18th, 2023, Seattle, WA, USA

https://urldefense.com/v3/__https://2023.ecoop.org/track/ftfjp-2023__;!!IBzWLUs!VGGRwrl7xjCbGyH86Z1Yr07U6CGdFAnZ5BBBnIzUoerjXelBPbLOhAy4ffB3iIJ-3hcxXG2QsDmcZ0C3lxaiJbfYn46ylF1khImN$
 
===

=== Important Dates ===

* Paper submission: May 22nd, 2023 (AoE)
* Author notification: June 23rd, 2023 (AoE)
* Workshop date: July 18th, 2023 (co-located with ECOOP 2023)

Deadlines expire at 23:59 anywhere on earth on the dates displayed above.
Submission site: 
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=ftfjp2023__;!!IBzWLUs!VGGRwrl7xjCbGyH86Z1Yr07U6CGdFAnZ5BBBnIzUoerjXelBPbLOhAy4ffB3iIJ-3hcxXG2QsDmcZ0C3lxaiJbfYn46ylMGqfB3W$
 

=== Objectives and Scope ===

Formal techniques can help analyse programs, precisely describe program
behaviour, and verify program properties. Modern programming languages
are interesting targets for formal techniques due to their ubiquity and
wide user base, stable and well-defined interfaces and platforms, and
powerful (but also complex) libraries. New languages and applications in
this space are continually arising, resulting in new programming
languages (PL) research challenges.

Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each other. FTfJP
is an established workshop which has run annually since 1999 alongside
ECOOP, with the goal of bringing together people working in both fields.

The workshop has a broad PL theme. The most important criterion is that
submissions will generate interesting discussions within this community.
The term "Java-like" is somewhat historic and should be interpreted
broadly: FTfJP solicits and welcomes submissions relating to programming
languages in general, beyond Java, including submissions related to C#,
Scala, and similar languages, and submissions on more general topics
that may be relevant to such languages.

Example topics of interest include:

* Language design and semantics
* Type systems
* Concurrency and new application domains
* Specification and verification of program properties
* Program analysis (static or dynamic)
* Program synthesis
* Security
* Pearls (programs or proofs)

FTfJP welcomes submissions on technical contributions, case studies,
experience reports, challenge proposals, and position papers.

Webpages for previous workshops in this series are available at:
https://urldefense.com/v3/__https://ftfjp.github.io/__;!!IBzWLUs!VGGRwrl7xjCbGyH86Z1Yr07U6CGdFAnZ5BBBnIzUoerjXelBPbLOhAy4ffB3iIJ-3hcxXG2QsDmcZ0C3lxaiJbfYn46ylBZLQXKk$
 

=== Paper Categories ===

Contributions are sought in two categories:

* Full Papers (6 pages, excluding references) present a technical
   contribution, case study, or detailed experience report. We welcome
   both complete and incomplete technical results; ongoing work is
   particularly welcome, provided it is substantial enough to stimulate
   interesting discussions.

* Short Papers (2 pages, excluding references) should advocate a
   promising research direction, or otherwise present a position likely
   to stimulate discussion at the workshop. We encourage, e.g.,
   established researchers to set out a personal vision, and beginning
   researchers to present a planned path to a Ph.D.

Both types of contributions will benefit from feedback received at the
workshop. Submissions will be peer reviewed, and will be evaluated based
on their clarity and their potential to generate interesting
discussions. Reviewing will be single blind, there is no need to
anonymize submissions.

The format of the workshop encourages interaction. FTfJP is a forum in
which a wide range of people share their expertise, from experienced
researchers to beginning PhD students.

=== Submission Guidelines ===

All submissions and reviews will be managed within EasyChair.
Submissions should be made via

https://urldefense.com/v3/__https://easychair.org/conferences/?conf=ftfjp2023__;!!IBzWLUs!VGGRwrl7xjCbGyH86Z1Yr07U6CGdFAnZ5BBBnIzUoerjXelBPbLOhAy4ffB3iIJ-3hcxXG2QsDmcZ0C3lxaiJbfYn46ylMGqfB3W$
 

There is no need to indicate the paper category (long/short).

Submissions should be in acmart/sigplan style, 10pt font. Formatting
requirements are detailed on the SIGPLAN Author Information page
(https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author__;!!IBzWLUs!VGGRwrl7xjCbGyH86Z1Yr07U6CGdFAnZ5BBBnIzUoerjXelBPbLOhAy4ffB3iIJ-3hcxXG2QsDmcZ0C3lxaiJbfYn46ylPjjyMP3$
 ).

We plan that, as in previous years, accepted papers will be published in
the ACM Digital Library, though authors will be able to opt out of this
publication, if desired. At least one author of an accepted paper must
register to 

[TYPES/announce] 2nd Call for presentations: 2023 Coq workshop

[Yves Bertot]

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

We are pleased to invite you to submit presentation proposals for the 
Coq Workshop 2023, which will be held in Białystok, Poland on July 31, 
2023, as a satellite to the ITP conference.


https://urldefense.com/v3/__https://coq-workshop.gitlab.io/2023/__;!!IBzWLUs!X_sYFMo_a1qe2a9T3xFecgAioGJwsNC2QtmKfb5RsuE0_sGgs3pl33kApYuOGqAAiph_VR8s9U2jYpMu-rGMwxDwaBYP0a8rugpA$ 



The Coq Workshop 2023 is the 14th installment of the Coq Workshop 
series. The workshop brings together users, contributors, and developers 
of the Coq proof assistant.


The Coq Workshop focuses on strengthening the Coq community and 
providing a forum for discussing practical issues, including the future 
of the Coq software, piece of software based on type theory and its 
associated ecosystem of libraries and tools. Thus, rather than serving 
as a venue for traditional research papers, the workshop is organized 
around informal presentations and discussions, supplemented with invited 
talks.



Important dates:

    May 26, 2023 (AoE): Deadline for submission of presentation proposals
    June 15, 2023: Notification to authors
    July 31, 2023: Workshop

Submission instructions:

Authors should submit presentation proposals as extended abstracts
through EasyChair.

Relevant subject matter includes but is not limited to:

    Language or tactic features for Coq
    Theory and implementation of the Calculus of Inductive Constructions
    Applications of Coq and experience reports on Coq use in education and
 industry
    Tools and platforms built on Coq
    Plugins and libraries for Coq
    Interfacing with Coq
    Formalization tricks and Coq pearls

Submission format:

Presentation proposals should be no more than 2 pages in length
including bibliographic references, and should use the EasyChair style
with the fullpage package. All submissions must be in PDF format.

Program committee:

    Nada Amin (Harvard)
    Jesper Bengtson (IT-University of Copenhagen)
    Yves Bertot (Inria) [chair]
    Ana Borges (University of Barcelona)
    Chantal Keller (LMF, Université Paris-Saclay)
    Pierre Roux (ONERA, Toulouse)
    Takafumi Saikawa (Nagoya University)
    Enrico Tassi (Inria) [chair]

Organizers and contact:

Enrico Tassi and Yves Bertot (coq2...@easychair.org)

[TYPES/announce] Conference in honour of Corrado Böhm

[Ronchi Della Rocca Simona]

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

The Accademia delle Scienze di Torino organizes a 

Conference in honour of Corrado Böhm

in occasion of the centenary of his birth.

Date: May 24, 2023.

For further information:

https://urldefense.com/v3/__https://www.accademiadellescienze.it/iniziative/2023/ricordando-corrado-bohm__;!!IBzWLUs!QnOVWluTadzMVtJz0xG3Brg4IHqOI7m8OYyFwjhRjOCRa_8OUwMUFcTpdllSGCsB1BVbcwDescXmQZK_DATCf_zTfAVL51pN$
  


_
Simona Ronchi Della Rocca
Professor Emerita 
of Theoretical Computer Science
Università di Torino
Accademia delle Scienze di Torino

[TYPES/announce] ICFP 2023: Call for Tutorial, Panel, and Discussion Proposals

[ICFP Publicity]

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

ICFP 2023
CALL FOR TUTORIAL, PANEL, AND DISCUSSION PROPOSALS
28th ACM SIGPLAN International Conference on Functional Programming


September 4 - 9, 2023
Seattle, WA, USA
https://urldefense.com/v3/__https://icfp23.sigplan.org/__;!!IBzWLUs!Xn8FNGF0gG7I2WNfEx7UhCWwIwbquhO6VXefumtkcbCz-8I0Zj33YHjeXPEv4rTWchKr-2eLEY8YHA9u_hbOQR73UDyIpDc_gn-GjO-Dtuw$
 


The 28th ACM SIGPLAN International Conference on Functional
Programming will be held in Seattle, WA, USA on September 4 - 9,
2023, with the option of virtual participation. ICFP provides a forum
for researchers and developers to hear about the latest work on the
design, implementations, principles, and uses of functional
programming.

Proposals are invited for tutorials, lasting approximately 3 hours each,
to be presented during ICFP and its co-located workshops and other events.
The tutorials may target an audience who is interested in commercial uses
of functional programming, but we also welcome tutorials whose primary
audience is researchers rather than practitioners. Tutorials may focus either
on a concrete technology or on a theoretical or mathematical tool. Ideally,
tutorials will have a concrete result, such as "Learn to do X with Y"
rather than "Learn language Y".

Just like last year, following the success of the #ShutDownPL event, we are also
inviting proposals for panels and discussions on topics of broader interest
to the PL community.

Tutorials, panels, and discussions may occur before or after ICFP,
co-located with the associated workshops, on September 4 or September 8-9.


--

Submission details

Deadline for submission: May 23rd, 2023
Notification of acceptance: May 26th, 2023

Prospective organizers of tutorials are invited to submit a completed
tutorial proposal form in plain text format to the ICFP 2023 workshop
co-chairs (Arthur Azevedo de Amorim and Yannick Forster), via email to

icfp-workshops-2023 AT googlegroups.com

by May 23rd, 2023. Please note that this is a firm deadline.

The proposal form is available at:

https://urldefense.com/v3/__http://www.icfpconference.org/icfp2023-files/icfp23-panel-form.txt__;!!IBzWLUs!Xn8FNGF0gG7I2WNfEx7UhCWwIwbquhO6VXefumtkcbCz-8I0Zj33YHjeXPEv4rTWchKr-2eLEY8YHA9u_hbOQR73UDyIpDc_gn-G-2IPkQU$
 
https://urldefense.com/v3/__http://www.icfpconference.org/icfp2023-files/icfp23-tutorials-form.txt__;!!IBzWLUs!Xn8FNGF0gG7I2WNfEx7UhCWwIwbquhO6VXefumtkcbCz-8I0Zj33YHjeXPEv4rTWchKr-2eLEY8YHA9u_hbOQR73UDyIpDc_gn-GrRvuVdY$
 

--

Selection committee

The proposals will be evaluated by a committee comprising the
following members of the ICFP 2023 organizing committee, together
with the members of the SIGPLAN executive committee.

Workshop Co-Chair: Arthur Azevedo de Amorim (Boston University)
Workshop Co-Chair: Yannick Forster (Inria Nantes)
General Chair: Nikhil Swamy (Microsoft Research)
Program Chair: Sam Lindley (University of Edinburgh)

--

Further information

Any queries should be addressed to the workshop co-chairs (Arthur
Azevedo de Amorim and Yannick Forster), via email to
icfp-workshops-2023 AT googlegroups.com

[TYPES/announce] [CFP] Student Research Competition (SRC) at ICFP'23

[Daniel Hillerström]

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

ICFP 2023 Student Research Competition

   Call for Submissions


ICFP 2023 invites students to participate in the Student Research
Competition in order to present their research and get feedback from
prominent members of the programming language research community.

The SRC consists of three rounds:

* Submission of an extended abstract
* Poster session at ICFP 2023
* Finalists' presentations at ICFP 2023

During the first round students submit an extended abstract detailing
their research to be reviewed by the program committee. Those students
whose abstracts get accepted advance to the poster session round which
will take place during ICFP 2023. Winners of the poster session
advance to next round, where they will give a 5-minute presentation
about their work on the ICFP main stage in front of a live audience.

### IMPORTANT DATES

* Submission Deadline: 25 May 2023 (Thursday)
* Author Notification: 15 June 2023 (Thursday)
* ICFP 2023 Conference in Seattle, Washington, USA:
4 September 2023 (Monday) - 9 September 2023 (Saturday)

### SUBMISSION OF EXTENDED ABSTRACTS

* Submission Website: https://urldefense.com/v3/__https://icfp23src.hotcrp.com__;!!IBzWLUs!VmtxbTN2rigExQ7lFKsWcmbobrr9loBWAqMq8fV3VyVUfFGB-TLOOwbMZmVcmUiFdrKQEa-dd8zkUlvyT8DbQUkfxzcEPG3rIeJGdJfBK1U$ 


Each submission (referred to as "abstract" below) should include the
student author's name and e-mail address; institutional affiliation;
research advisor's name; ACM student member number; category
(undergraduate or graduate); research title; and an extended abstract
addressing the following:

* Problem and Motivation: Clearly state the problem being addressed and
  explain the reasons for seeking a solution to this problem.

* Background and Related Work: Describe the specialized (but
  pertinent) background necessary to appreciate the work in the
  context of ICFP areas of interest. Include references to the
  literature where appropriate, and briefly explain where your work
  departs from that done by others.

* Approach and Uniqueness: Describe your approach in addressing the
  problem and clearly state how your approach is novel.

* Results and Contributions: Clearly show how the results of your work
  contribute to programming language design and implementation in
  particular and to computer science in general; explain the
  significance of those results.

* Submissions must be original research that is not already published
  at ICFP or another conference or journal. One of the goals of the
  SRC is to give students feedback on ongoing, unpublished
  work. Furthermore, the abstract must be authored solely by the
  student. If the work is collaborative with others and/or part of a
  larger group project, the abstract should make clear what the
  student's role was and should focus on that portion of the work.

* Formatting: Submissions must be in PDF format, printable in black
  and white on US Letter sized paper, and interpretable by common PDF
  tools. All submissions must adhere to the "ACM Small" template that
  is available (in both LaTeX and Word formats) from
  
https://urldefense.com/v3/__https://www.acm.org/publications/authors/submissions__;!!IBzWLUs!VmtxbTN2rigExQ7lFKsWcmbobrr9loBWAqMq8fV3VyVUfFGB-TLOOwbMZmVcmUiFdrKQEa-dd8zkUlvyT8DbQUkfxzcEPG3rIeJGFjWuI_U$
 . For authors
  using LaTeX, a lighter-weight package, including only the essential
  files, is available from
  
https://urldefense.com/v3/__http://sigplan.org/Resources/Author/*acmart-format__;Iw!!IBzWLUs!VmtxbTN2rigExQ7lFKsWcmbobrr9loBWAqMq8fV3VyVUfFGB-TLOOwbMZmVcmUiFdrKQEa-dd8zkUlvyT8DbQUkfxzcEPG3rIeJG8wR2mFE$
 . The submission
  must not exceed 3 pages in PDF format. Reference lists do not count
  towards the 3-page limit.

Further information is available at the ICFP SRC website:
https://urldefense.com/v3/__https://icfp23.sigplan.org/track/icfp-2023-student-research-competition__;!!IBzWLUs!VmtxbTN2rigExQ7lFKsWcmbobrr9loBWAqMq8fV3VyVUfFGB-TLOOwbMZmVcmUiFdrKQEa-dd8zkUlvyT8DbQUkfxzcEPG3rIeJGLBghl5A$ 


### PROGRAM COMMITTEE

Daniel Hillerström (Huawei Research Center Zurich) (co-chair)
J. Garrett Morris (University of Iowa) (co-chair)
Kathy Gray (Meta)
Leo Stefanesco (MPI-SWS)
Shin-Cheng Mu (Academia Sinica)

The University of Edinburgh is a charitable body, registered in Scotland, with 
registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh 
Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

[TYPES/announce] Assistant Professor in Theoretical Foundations of AI at Chalmers University of Technology

[Ana Bove]

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

TheComputer Science and Engineering departmentat Chalmers University of 
Technology, Sweden,is currently seeking applications for the position of 
Assistant Professor in Theoretical Foundations of AI.


This is a tenure track positionwhichoffers the opportunity to shape the 
future ofarapidly evolving discipline,with a start-up package that also 
covers the funding of additional group members.


The department is particularly interested in candidates who can 
demonstrate a strong theoretical grounding inComputer Science, as well 
as an ability to inspire and engage students.


The full details of the position, including the application procedure 
and deadline, can be found onourwebsite:


Assistant Professor in Theoretical Foundations of AI 



Pleasepass this information to people who might be interested in the 
position. Alternatively, if thisopportunity aligns with your own 
research interests,don’t hesitate to submityour application.


Thanks!

--
-- Ana Bove, Docent
Phone: (46)(31) 772 1020
https://urldefense.com/v3/__http://www.cse.chalmers.se/*bove__;fg!!IBzWLUs!WOwnGTbE4-ZUqR82_KZl2mv0pw63FS6-Qv0zWpwwgL4dCKZ2sCqlSJlHN8lNzmCWzVn-FoV4fvRVwIYXHsVs8mujJMfJxw$ 
Department of Computer Science and Engineering

Chalmers Univ. of Technology and Univ. of Gothenburg

[TYPES/announce] LICS 2023 Call for Participation

[Sam Staton]

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

CALL FOR PARTICIPATION 

Thirty-Eighth Annual ACM/IEEE Symposium on
LOGIC IN COMPUTER SCIENCE (LICS)
26 June – 29 June 2023
preceded by workshops 24-25 June 2023
https://urldefense.com/v3/__https://lics.siglog.org/lics23/__;!!IBzWLUs!U7pofNqykcqBmLXFO-3oz6Y4bVmd901x5eqMuz7ffYz4hh3wzRnb0Phn7nKD6qUZ5SAejcaEQou1syP_-nBXrwWnva_ZrWD8aMed6Q$
 

Early registration ends 12 May 2023
Student travel grants deadline 8 May 2023

Do book accommodation sooner rather than later. Boston can be expensive and 
there is another big event on 25 June. 

Invited talks and tutorials from Adnan Darwiche, Azadeh Farzan, Dale Miller, 
Toniann Pitassi, Dan Suciu
Full programme at 
https://urldefense.com/v3/__https://lics.siglog.org/lics23/program.html__;!!IBzWLUs!U7pofNqykcqBmLXFO-3oz6Y4bVmd901x5eqMuz7ffYz4hh3wzRnb0Phn7nKD6qUZ5SAejcaEQou1syP_-nBXrwWnva_ZrWAePJ8r9Q$
 

Workshops:
Combinatorial games in finite model theory
The decision problem in first order logic (DPFO 2023)
International Workshop on Quantitative Logical Methods (Qualog)
Structure meets power
Logic mentoring workshop (LMW)

[TYPES/announce] DEADLINE EXTENSION — Call for Nominations: E. W. Beth Outstanding Dissertation Prize 2023

[Ana Sokolova]

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

The extended deadline for nominations is the *30th of May 2023*.
——--
Since 2002, the Association for Logic, Language, and Information (FoLLI)
has been awarding the annual E.W. Beth Dissertation Prize to outstanding
Ph.D. dissertations in Logic, Language, and Information (
https://urldefense.com/v3/__http://www.folli.info/?page_id=74__;!!IBzWLUs!XJvVcv7gy_KxPjYljPeVIZzcXyfRygWAv_1qzWIytvCln0qcRN_IjkfWroOi5zhpkS9jq1waHcN-9XucT8Q26UvVu7MMs9RMiz8A$
 ), with financial support of the E.W. Beth
Foundation (
https://urldefense.com/v3/__https://www.knaw.nl/en/awards/funds/evert-willem-beth-stichting/evert-willem-beth-foundation__;!!IBzWLUs!XJvVcv7gy_KxPjYljPeVIZzcXyfRygWAv_1qzWIytvCln0qcRN_IjkfWroOi5zhpkS9jq1waHcN-9XucT8Q26UvVu7MMs8GUJDAK$
 ).
Nominations are now invited for the best dissertation in these areas
resulting in a Ph.D. degree awarded in 2022.
——--
Qualifications:

 - A Ph.D. dissertation on a topic concerning Logic, Language, or
Information is eligible for the Beth Dissertation Prize 2023, if the degree
was awarded  between January 1st and December 31st, 2022.
 - There are no restrictions on the nationality, ethnicity, age, gender or
employment status of the author of the nominated dissertation, nor on the
university, academic department or scientific institution formally
conferring the Ph.D. degree, nor on the language in which the dissertation
has originally been written.
 -  In accordance with the aim of the Beth Foundation to continue and
extend the work of the Dutch logician Evert Willem Beth, nominations are
invited of excellent dissertations on topics in the broad remit of ESSLLI,
including current topics in philosophical and mathematical logic, computer
science logic, philosophy of science, philosophy of language, history of
logic, history of the philosophy of science and scientific philosophy in
general, as well as the current theoretical and foundational developments
in information and computation, language, and cognition. Dissertations with
results more broadly impacting various research areas in their
interdisciplinary investigations are especially solicited.
 -  If a nominated dissertation has originally been written in a language
other than English, its dossier should still contain the required 10 page
English abstract, see below. If the committee decides that a nominated
dissertation in a language other than English requires translation to
English for proper evaluation, the committee can transfer its nomination to
the competition in 2024. The English translation must in such cases be
submitted before the deadline of the call for nominations in 2024. The
committee may recommend the Beth Foundation to consider supporting such
nominated dissertations for English translation, upon request by the author
of the dissertation.

The prize consists of:
 - a certificate
 - a donation of 3000 euros, provided by the E.W. Beth Foundation
 - an invitation to submit the dissertation, possibly after revision, for
publication in FoLLI Publications on Logic, Language and Information
(Springer).

Only digital submissions are accepted, without exception. Hard copy
submissions are not allowed. The following documents are to be submitted in
the nomination dossier:
 - The original dissertation in pdf format (ps/doc/rtf etc. not acceptable).
 - A ten-page English abstract of the dissertation, presenting the main
results of each chapter.
 - A letter of nomination from the dissertation supervisor, which concisely
describes the scope and significance of the dissertation, stating when the
degree was officially awarded and the members of the Ph.D. committee.
Nominations should contain the address, phone and email details of the
nominator.
 - Two additional letters of support, including at least one from a referee
not affiliated with the academic institution that awarded the Ph.D. degree,
nor otherwise related to the nominee (e.g. former teachers, supervisors,
co-authors, publishers or relatives) or the dissertation.
 - Self-nominations are not possible.

All pdf documents must be submitted electronically, *as one pdf file*, via
EasyChair by following the link
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=bodp23__;!!IBzWLUs!XJvVcv7gy_KxPjYljPeVIZzcXyfRygWAv_1qzWIytvCln0qcRN_IjkfWroOi5zhpkS9jq1waHcN-9XucT8Q26UvVu7MMswmWawyy$
 . In case of any problems or
questions please contact the chair of the committee Ana Sokolova (
a...@cs.uni-salzburg.at).

The prize will be awarded by the chair of the FoLLI board at a ceremony
during the 34th ESSLLI summer school in Ljubljana, July 31 - August 11,
2023.

Beth dissertation prize committee 2023:

Maria Aloni (University of Amsterdam)
Agata Ciabattoni (TU Wien)
Robin Cooper (University of Gothenburg)
Guy Emerson (University of Cambridge)
Herman Geuvers (Radboud University Nijmegen)
Erich Grädel (RWTH Aachen