[TYPES/announce] APLAS 2023 first Call for Papers

[Sato, Ryosuke]

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

==
CALL FOR PAPERS

21st Asian Symposium on Programming Languages and Systems (APLAS 2023)
Taipei, Taiwan, Sun 26 – Wed 29 November 2023

https://urldefense.com/v3/__https://conf.researchr.org/home/aplas-2023__;!!IBzWLUs!Q_kgAg7CnO59QyVLBawlsjljOIx5T7j_dakrrTHciqE5TZM8PKqpuTCEihppnrk8DK3Mzhi_fXlaNfEJ11Xn4JLpn_fTxMfNLu5Aew$
 
==


IMPORTANT DATES
-
Submission deadline: Thu 15 Jun 2023 AoE
Author response: Mon 31 Jul 12:00 - Wed 2 Aug 12:00 2023 AoE
Author notification: Mon 14 Aug 2023 AoE
Final paper deadline: Wed 6 Sep 2023 AoE
Conference: Sun 26 – Wed 29 Nov 2023


SCOPE
-
We solicit submissions in the form of regular research papers
describing original scientific research results, including system
development and case studies. Among others, solicited topics include:

- ** programming paradigms and styles ** :
functional programming; object-oriented programming; probabilistic
  programming; logic
  programming; constraint programming; extensible programming
  languages; programming languages for systems code; novel programming
  paradigms;

- ** methods and tools to specify and reason about programs and
  languages ** :

  programming techniques; meta-programming; domain-specific
  languages; proof assistants; type systems; dependent types; program
  logics, static and dynamic program analysis; language-based
  security; model checking; testing;

- ** programming language foundations ** :

  formal semantics; type theory; logical foundations; category
  theory; automata; effects; monads and comonads; recursion and
  corecursion; continuations and effect handlers; program
  verification; memory models; abstract interpretation;

- ** methods and tools for implementation ** :

  compilers; program transformations; rewriting systems;
  partial evaluation; virtual machines; refactoring; intermediate
  languages; run-time environments; garbage collection and memory
  management; tracing; profiling; build systems; program synthesis;

- ** concurrency and distribution ** :

  process algebras; concurrency theory; session types; parallel
  programming; service-oriented computing; distributed and mobile
  computing; actor-based languages; verification and testing of
  concurrent and distributed systems;

- ** applications and emerging topics ** :

  programming languages and PL methods in education, security,
  privacy, database systems, computational biology, signal
  processing, graphics, human-computer interaction, computer-aided
  design, artificial intelligence and machine learning; case
  studies in program analysis and verification.


GENERAL INFORMATION
-
Submissions should not exceed 17 pages, excluding bibliography in the
Springer LNCS format. LaTeX template is available at:

  
https://urldefense.com/v3/__https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines__;!!IBzWLUs!Q_kgAg7CnO59QyVLBawlsjljOIx5T7j_dakrrTHciqE5TZM8PKqpuTCEihppnrk8DK3Mzhi_fXlaNfEJ11Xn4JLpn_fTxMemsm2G9w$
 

The accepted papers will be allowed to use one extra page for the
content to accommodate feedback from the reviews in the final paper
versions.

Papers should be submitted via HotCRP:

  
https://urldefense.com/v3/__https://aplas2023.hotcrp.com/__;!!IBzWLUs!Q_kgAg7CnO59QyVLBawlsjljOIx5T7j_dakrrTHciqE5TZM8PKqpuTCEihppnrk8DK3Mzhi_fXlaNfEJ11Xn4JLpn_fTxMePy9Yl2Q$
 

The review process of APLAS 2023 is double-anonymous, with a rebuttal
phase. In your submission, please, omit your names and institutions;
refer to your prior work in the third person, just as you refer to
prior work by others; do not include acknowledgments that might
identify you.

Additional material intended for reviewers but not for publication in
the final version - for example, details of proofs - may be placed in
a clearly marked appendix that is not included in the page limit.
Reviewers are at liberty to ignore appendices and papers must be
understandable without them.

Submitted papers must be unpublished and not submitted for publication
elsewhere. Papers must be written in English. The proceedings will be
published as a volume in Springer’s LNCS series. Accepted papers must
be presented at the conference.


POSTERS and STUDENT RESEARCH COMPETITION


APLAS 2023 includes a Posters session and a Student Research
Competition. For more details, please see the website.

 
https://urldefense.com/v3/__https://conf.researchr.org/track/aplas-2023/posters-and-src__;!!IBzWLUs!Q_kgAg7CnO59QyVLBawlsjljOIx5T7j_dakrrTHciqE5TZM8PKqpuTCEihppnrk8DK3Mzhi_fXlaNfEJ11Xn4JLpn_fTxMcsKqKKWg$
 


ORGANIZERS
-

General Chair:

  

[TYPES/announce] Postdoc @ DTU Compute in Modelling and Verification of Concurrent & Distributed Applications

[Alceste Scalas]

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

We are looking for a postdoctoral researcher with experience in formal 
methods

for distributed systems and/or programming languages.

* Application deadline:  21 May 2023 (Danish time)
* Starting date: September  2023 (negotiable)
* Duration of the position:  2 years
* For inquiries, please contact:  Alceste Scalas 
* Application link with more information:

https://urldefense.com/v3/__https://efzu.fa.em2.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_1/job/1533__;!!IBzWLUs!XePA8klv4-7ewe1aYJ4VX-rnXLCc1zGwtsH7P_ryvyVUUbk_I1k281p4bhAjldKJtJwcGWpmTSq2qKPB-rxPepOiUROE$ 

The successful applicant will join the DTU Compute section on Software 
Systems

Engineering, which involves researchers in various areas of software
specification, verification, engineering, and security --- with a strong
emphasis on formal methods.


https://urldefense.com/v3/__https://www.compute.dtu.dk/english/research/research-sections/software-systems-engineering__;!!IBzWLUs!XePA8klv4-7ewe1aYJ4VX-rnXLCc1zGwtsH7P_ryvyVUUbk_I1k281p4bhAjldKJtJwcGWpmTSq2qKPB-rxPeujXTJ73$ 

This Postdoc pposition is part of the Horizon Europe project TaRDIS 
(Trustworthy

And Resilient Decentralised Intelligence for edge Systems -
).   The main research topics of this 
position

are:

1. new methods for modelling concurrent and distributed 
applications, based

   on practical industrial use cases; and

2. new methods for verifying the correctness of concurrent and 
distributed

   applications, based on the models at point 1.

The TaRDIS project is a collaboration between DTU (Denmark), NOVA University
Lisbon (Portugal, project coordinator), the University of Oxford (UK), the
University of Novi Sad (Serbia), the National and Kapodistrian University of
Athens (Greece), and 6 industry partners: Actyx AG (Germany), GMV Aerospace
(Spain), EDP NEW R (Portugal), Telefónica Research (Spain), Caixa Mágica
Software (Portugal), and Martel Innovate (Switzerland).


# RESPONSIBILITIES AND QUALIFICATIONS

Within the TaRDIS project, the DTU team's research focuses on modelling
distributed applications and verifying their properties, in particular
communication correctness and security.

Your main tasks within this project will be:

* closely collaborate with the DTU faculty members and the two PhD 
students

  involved in the TaRDIS project;

* study the project's industrial use cases;

* actively contribute to the technical discussions with the project 
partners
  (both industrial and academic), and work towards the project 
deliverables;


* acquire the necessary expertise in state-of-the-art research in 
formal
  methods for modelling and verifying distributed applications --- 
with a

  focus on correctness, safety, and reliability;

* explore new methods to ensure the correctness of distributed 
applications.

  You will play a key role in developing the necessary theory and in
  implementing software tools based on such theory.

You will also have the opportunity to co-supervise MSc or BSc student 
projects

related to your research.

To be considered for the position, you need to document your research 
experience
with formal methods for programming languages and/or distributed 
systems.  You

will also need to document your programming skills --- preferably including
functional programming, and some experience in developing distributed
applications.


# ASSESSMENT OF THE APPLICANTS

The assessment of the applicants will take place no later than the 
second half
of May 2023 --- but if you apply for this position, you may be contacted 
for an
earlier interview (before the application deadline).  If you decide to 
apply,

please contact us.


# FURTHER INFORMATION

Application link with more information about this position:


https://urldefense.com/v3/__https://efzu.fa.em2.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_1/job/1533__;!!IBzWLUs!XePA8klv4-7ewe1aYJ4VX-rnXLCc1zGwtsH7P_ryvyVUUbk_I1k281p4bhAjldKJtJwcGWpmTSq2qKPB-rxPepOiUROE$ 


For further information and inquiries, please contact:

Alceste Scalas 

You can read more about DTU Compute at 
.

If you are applying from abroad, you may find useful information on 
working in

Denmark and at DTU at:

https://urldefense.com/v3/__https://www.dtu.dk/english/about/job-and-career/moving-to-denmark__;!!IBzWLUs!XePA8klv4-7ewe1aYJ4VX-rnXLCc1zGwtsH7P_ryvyVUUbk_I1k281p4bhAjldKJtJwcGWpmTSq2qKPB-rxPehdSj1As$ 


--
Alceste Scalas  - 

[TYPES/announce] TbiLLC 2023: Final Deadline Extension Mon 3 April 2023 AoE

[Hansen, H.H.]

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

THE FOURTEENTH INTERNATIONAL TBILISI SYMPOSIUM
ON LOGIC, LANGUAGE AND COMPUTATION

18-22 September, 2023
Telavi, Georgia
Website: 
https://urldefense.com/v3/__https://events.illc.uva.nl/Tbilisi/Tbilisi2023/__;!!IBzWLUs!TsK-WbY0CNqCRj8ba_yijRXeMYTUq_M8YICLj80805pTd5w-X9F5-P-A-YUQbKt4d7C6ZvFS54DmvFF7guNdingLhFM_grb33w$
 
***
THIRD CALL FOR PAPERS: FINAL DEADLINE EXTENSION 3 APRIL 2023
-- UPDATED: Workshops, Important Dates --

The Fourteenth International Tbilisi Symposium on Logic, Language, and
Computation (TbiLLC 2023) will be held 18-22 September 2023 in Telavi,
located in the Kakheti region, Georgia, north-east of Tbilisi. TbiLLC 2023
will be preceded by Logic, Algebra and Truth Degrees (LATD 2023) and DaLí -
Dynamic Logic: new trends and applications (DaLi 2023).

The Programme Committee invites submissions for contributions on all
aspects of logic, language, and computation. Work of an interdisciplinary
nature is particularly welcome. Areas of interest include, but are not
limited to:

* Natural language syntax, semantics, and pragmatics
* Linguistic typology and semantic universals
* Language evolution and learnability
* Variability in language
* Sociolinguistics
* Historical linguistics, history of logic
* Natural logic, inference and entailment in natural language
* Natural language processing
* Distributional and probabilistic models of information, meaning and
computation
* Logic, games, and formal pragmatics
* Logic and cognition
* Logics for artificial intelligence and computer science
* Knowledge representation
* Foundations of machine learning
* Formal models of multiagent systems
* Logics for social networks
* Logics for knowledge, belief, and information dynamics
* Computational social choice
* Information retrieval, query answer systems
* Constructive, intuitionistic, modal and other non-classical logics
* Algebraic and coalgebraic logic and semantics
* Categorical logic
* Models of computation

PROGRAMME

The programme will include the following tutorials and a series of invited
lecturers.

*Tutorial speakers*
Language: Peter Sutton (UPF, Barcelona)
Logic & Computation: Frank Wolter (University of Liverpool)

*Invited speakers*
Language:
 - Heather Burnett (CNRS-LLF, Paris)
 - Stephanie Solt (ZAS, Berlin)
Logic & Computation:
 - Balder ten Cate (University of Amsterdam)
 - Nina Gierasimczuk (Technical University of Denmark)

WORKSHOPS

There will be two workshops embedded in the conference programme:

"The Semantics of Hidden Meanings"
Organisers: Heather Burnett (CNRS-LLF, Paris), Stephanie Solt (ZAS,
Berlin), Peter Sutton (UPF, Barcelona)
Invited speaker:
- Elin McCready (Aoyama Gakuin University)
For more details see the workshop webpage:
https://urldefense.com/v3/__https://sites.google.com/view/hidden-meanings__;!!IBzWLUs!TsK-WbY0CNqCRj8ba_yijRXeMYTUq_M8YICLj80805pTd5w-X9F5-P-A-YUQbKt4d7C6ZvFS54DmvFF7guNdingLhFOTgqVFtw$
 

and

"Learning and Logic"
Organisers: Balder ten Cate (University of Amsterdam) and Aybüke Özgün
(University of Amsterdam).
Invited speakers:
 - Victor Dalmau (UPF Barcelona),
 - Konstantin Genin (University of Tübingen),
 - Dick de Jongh (University of Amsterdam),
 - Ana Ozaki (University of Bergen)
For more details see the workshop webpage:
https://urldefense.com/v3/__https://sites.google.com/view/lealog/home__;!!IBzWLUs!TsK-WbY0CNqCRj8ba_yijRXeMYTUq_M8YICLj80805pTd5w-X9F5-P-A-YUQbKt4d7C6ZvFS54DmvFF7guNdingLhFNCCrf8uQ$
 

PROGRAMME COMMITTEE CHAIRS

Berit Gehrke (Humboldt-Universität zu Berlin, DE)
Helle Hvid Hansen (University of Groningen, NL)

PROGRAMME COMMITTEE

Samson Abramsky (University College London, UK)
Philippe Balbiani (CNRS & University of Toulouse, FR)
Guram Bezhanishvili (New Mexico State University, USA)
Nick Bezhanishvili (University of Amsterdam, NL)
Olga Borik (Universidad Nacional de Educación a Distancia, ES)
Zoé Christoff (University of Groningen, NL)
Agata Ciabattoni (TU Wien, AT)
Milica Denić (Tel Aviv University, IL)
David Gabelaia (Javakhishvili Tbilisi State University, GE)
Berit Gehrke (Humboldt-Universität zu Berlin, DE, co-chair)
Jim de Groot (Australian National University, AU)
Helle Hvid Hansen (University of Groningen, NL, co-chair)
Daniel Hole (University of Stuttgart, DE)
Rosalie Iemhoff (Utrecht University, NL)
Maarten Janssen (Charles University, Prague, CZ)
Clemens Kupke (University of Strathclyde, UK)
Temur Kutsia (Johannes Kepler University Linz, AT)
Mora Maldonado (CNRS & University of Nantes, FR)
Louise McNally (Universitat Pompeu Fabra, Barcelona, ES)
Lawrence Moss (Indiana University, USA)
Aybüke Özgün (University of Amsterdam, NL)
Mehrnoosh Sadrzadeh (University College London, UK)
Viola Schmitt (Humboldt-Universität zu Berlin, DE)
Todd Snider (Heinrich Heine University of Düsseldorf, DE)
Ana Sokolova (University of Salzburg, AT)
Luca Spada 

[TYPES/announce] TyDe 2023 - Call for Papers

[Youyou Cong]

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


 CALL FOR PAPERS

 8th Workshop on Type-Driven Development (TyDe 2023)
 Co-Located with ICFP 2023 (Seattle, Washington, USA)

 
https://urldefense.com/v3/__https://icfp23.sigplan.org/home/tyde-2023__;!!IBzWLUs!XzhHqmYiGDXG6yucxe8_8sVTBKyD4RFe9FQISgGYj2Zrngi4p48pF9Q9bB2ZkDl_6EGerN8mx2GbY58PgOG8ZmhUMO4z8uGk$
 


# Goals of the Workshop

The Workshop on Type-Driven Development (TyDe) aims to show how
static type information may be used effectively in the development
of computer programs. Co-located with ICFP, this workshop brings
together leading researchers and practitioners who are using or
exploring types as a means of program development.

We welcome all contributions, both theoretical and practical, on a
range of topics including:

- dependently typed programming;
- generic programming;
- design and implementation of programming languages, exploiting
  types in novel ways;
- exploiting typed data, data dependent data, or type providers;
- static and dynamic analyses of typed programs;
- tools, IDEs, or testing tools exploiting type information;
- pearls, being elegant, instructive examples of types used in the
  derivation, calculation, or construction of programs.

# Proceedings and Copyright

We will have formal proceedings, published by the ACM. Accepted
papers will be included in the ACM Digital Library. Authors must
grant ACM publication rights upon acceptance, but may retain
copyright if they wish. Authors are encouraged to publish auxiliary
material with their paper (source code, test data, and so forth).
The proceedings will be freely available for download from the ACM
Digital Library from one week before the start of the conference
until two weeks after the conference.

The official publication date is the date the papers are made
available in the ACM Digital Library. This date may be up to two
weeks prior to the first day of the conference. The official
publication date affects the deadline for any patent filings related
to published work.

# Submission Details

Submissions should fall into one of two categories:

- regular research papers (12 pages);
- extended abstracts (3 pages).

The bibliography will not be counted against the page limits for
either category.

Regular research papers are expected to present novel and interesting
research results, and will be included in the formal proceedings.
Extended abstracts should report work in progress that the authors
would like to present at the workshop. Extended abstracts will be
distributed to workshop attendees but will not be published in the
formal proceedings.

We welcome submissions from PC members (with the exception of the two
co-chairs), but these submissions will be held to a higher standard.

Submission is handled through HotCRP:

  
https://urldefense.com/v3/__https://tyde23.hotcrp.com__;!!IBzWLUs!XzhHqmYiGDXG6yucxe8_8sVTBKyD4RFe9FQISgGYj2Zrngi4p48pF9Q9bB2ZkDl_6EGerN8mx2GbY58PgOG8ZmhUMPKpgJyi$
 

All submissions should be in portable document format (PDF) and
formatted using the ACM SIGPLAN style guidelines:

  
https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!XzhHqmYiGDXG6yucxe8_8sVTBKyD4RFe9FQISgGYj2Zrngi4p48pF9Q9bB2ZkDl_6EGerN8mx2GbY58PgOG8ZmhUMKurdkGe$
 

Note that submissions should use the new 'acmart' format and the
two-column 'sigplan' subformat (not to be confused with the
one-column 'acmsmall' subformat).

Extended abstracts must be submitted with the label 'Extended
Abstract' clearly in the title.

# Participant Support

Student attendees with accepted papers can apply for a SIGPLAN PAC
grant to help cover participation-related expenses. PAC also offers
other support, such as for child-care expenses during the meeting or
for accommodations for members with physical disabilities. For
details on the PAC program, see its web page:

  
https://urldefense.com/v3/__https://www.sigplan.org/PAC/__;!!IBzWLUs!XzhHqmYiGDXG6yucxe8_8sVTBKyD4RFe9FQISgGYj2Zrngi4p48pF9Q9bB2ZkDl_6EGerN8mx2GbY58PgOG8ZmhUMG7d7wLb$
 

# Important Dates

- Submission Deadline: Thursday June 1, 2023
- Author Notification: Thursday June 29, 2023
- Camera-Ready Deadline: Thursday July 13, 2023
- Workshop: Monday September 4, 2023

# Workshop Organization

Organizing Committee:
- Youyou Cong (Tokyo Institute of Technology, Japan)
- Pierre-Evariste Dagand (IRIF / CNRS, France)

Program Committee:
- Reynald Affeldt (AIST, Japan)
- Sandra Alves (DCC-FCUP, Portugual)
- Stephen Chang (UMass Boston, United States)
- Magnus Madsen (Aarhus University, Denmark)
- Victor Cacciari Miraldo (Channable, Netherlands)
- Jonathan Protzenko (Microsoft Research, United States)
- Marianna Rapoport (Amazon Web Services, Canada)
- Christine Rizkallah (University of Melbourne, Australia)

[TYPES/announce] Final Call for Papers: Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'23)

[Carlos Olarte]

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

[Apologies if you receive multiple copies of this CFP. Please forward to
interested parties]

===

Final call for papers -- LFMTP 2023

   Logical Frameworks and Meta-Languages:
   Theory and Practice

 Rome, Italy -- July 2nd, 2023
   Affiliated with FSCD 2023

  
https://urldefense.com/v3/__https://lfmtp.org/workshops/2023__;!!IBzWLUs!WijlnDHxireQPAptjL3kx30kZPHdkUxtjymFHtpIV7KeSAZ8j6kdpN3xptDwFWWtIOPkJfoJ9GCIuMxtxg5fBkYcwFNrH9yRh8qTHw$
 

===

Logical frameworks and meta-languages form a common substrate for
representing, implementing and reasoning about a wide variety of
deductive systems of interest in logic and computer science. Their
design, implementation and their use in reasoning tasks, ranging from
the correctness of software to the properties of formal systems,
have been the focus of considerable research over the last two decades.
This workshop will bring together designers, implementors and
practitioners to discuss various aspects impinging on the structure and
utility of logical frameworks, including the treatment of variable
binding, inductive and co-inductive reasoning techniques and the
expressiveness and lucidity of the reasoning process.

LFMTP 2023 will provide researchers a forum to present state-of-the-art
techniques and discuss progress in areas such as the following:

* Encoding and reasoning about the meta-theory of programming languages,
  logical systems and related formally specified systems.

* Theoretical and practical issues concerning the treatment of variable
  binding, especially the representation of, and reasoning about,
  datatypes defined from binding signatures.

* Logical treatments of inductive and co-inductive definitions and
  associated reasoning techniques, including inductive types of higher
  dimension in homotopy type theory.

* Graphical languages for building proofs, applications in geometry,
  equational reasoning and category theory.

* New theory contributions: canonical and substructural frameworks,
  contextual frameworks, proof-theoretic foundations supporting
  binders, functional programming over logical frameworks,
  homotopy and cubical type theory.

* Applications of logical frameworks: proof-carrying architectures,
  proof exchange and transformation, program refactoring, etc.

* Techniques for programming with binders in functional programming
  languages such as Haskell, OCaml or Agda, and logic programming
  languages such as lambda Prolog or Alpha-Prolog.

The workshop's program will include contributed and invited talks.
We hope that LFMTP takes place physically in Rome, but online
participation will be possible and may even be necessary.

## Important Dates

Abstract submission deadline: April 10
Paper submission deadline: April 20
Notification to authors: May 20

## Submission

Submit on EasyChair: 
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=lfmtp23__;!!IBzWLUs!WijlnDHxireQPAptjL3kx30kZPHdkUxtjymFHtpIV7KeSAZ8j6kdpN3xptDwFWWtIOPkJfoJ9GCIuMxtxg5fBkYcwFNrH9zIUJliJQ$
 

All papers must be original and not simultaneously submitted to another
journal or conference.

In addition to regular papers, we welcome/encourage the submission of
"work in progress" reports, in a broad sense. Those do not need to
report fully polished research results, but should be of interest for
the community at large.

Submitted papers should be in PDF, formatted using the EPTCS style
guidelines 
(https://urldefense.com/v3/__https://info.eptcs.org/__;!!IBzWLUs!WijlnDHxireQPAptjL3kx30kZPHdkUxtjymFHtpIV7KeSAZ8j6kdpN3xptDwFWWtIOPkJfoJ9GCIuMxtxg5fBkYcwFNrH9xlvfZc7Q$
 ). The length is restricted to 15
pages for regular papers and 8 pages for "work in progress" papers
(both limits include references).

## Proceedings

A selection of the presented papers will be published online in the
Electronic Proceedings in Theoretical Computer Science (EPTCS).

## Invited Speakers

- Niki Vazou (IMDEA Software Institute Madrid, Spain)

Note: shared session with LSFA'23 
(https://urldefense.com/v3/__https://sites.google.com/ufg.br/lsfa2023__;!!IBzWLUs!WijlnDHxireQPAptjL3kx30kZPHdkUxtjymFHtpIV7KeSAZ8j6kdpN3xptDwFWWtIOPkJfoJ9GCIuMxtxg5fBkYcwFNrH9z2bqA6-w$
 
).

## Program Committee

* Roberto Blanco (MPI-SP)
* Frédéric Blanqui (Inria)
* Ana Bove (Chalmers University of Technology)
* Alberto Ciaffaglione, co-chair (Università degli Studi di Udine)
* Amy Felty (University of Ottawa)
* Assia Mahboubi (Inria)
* Narciso Marti-Oliet (Universidad Complutense de Madrid)
* Gopalan Nadathur (University of Minnesota)
* Carlos Olarte, co-chair (LIPN, Université Sorbonne Paris Nord)
* Clément Pit-Claudel (Amazon AWS)
* Andrei Popescu (University of Sheffield)
* Claudio Sacerdoti Coen 

[TYPES/announce] Postdoc position on design and/or verification of distributed systems at the University of Birmingham, UK

[vincent rahli]

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

Dear all,

We would like to invite applications for an up to 3 years fully-funded
postdoctoral position within the School of Computer Science at the
University of Birmingham (see below for details on how to apply).

The successful candidate will contribute to an EPSRC-funded project aiming
at designing and formally verifying distributed systems, in particular
Byzantine fault-tolerant distributed systems as used for example in
blockchain technology.

The environment:


The School of Computer Science has large and thriving Theory and Security
research groups. Among our research interests related to this project are
for example:
   - Formal verification
   - Proof assistants
   - Model checking
   - Blockchain Technology
   - Security & Privacy

Both groups are very active, organising regular seminars, informal
meetings, and actively participating in many events such as the Midlands
Graduate School or the Cyber Security PhD Winter School. For more
information see
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3Xr3nfQpA$
 
and
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/centre-for-cyber-security-and-privacy/index.aspx__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3XSKLSctQ$
 
.

How to apply:
-

Interested people are encouraged to contact me by email (v.ra...@bham.ac.uk)
to discuss their research interests and details of the positions. Further
information on how to apply is available here:
https://urldefense.com/v3/__https://edzz.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_6001/job/521/?utm_medium=jobshare__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3U_X8mBgg$
 

Best,
Vincent Rahli

-- 
https://urldefense.com/v3/__https://vrahli.github.io/__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3Xx2mKSMg$
 

[TYPES/announce] IFL23 first CFP

[Pieter Koopman]

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

*Call for papers*

The 35th Symposium on Implementation and Application of Functional
Languages (IFL 2023)

Braga, Portugal, August 29th-August 31st, 2023
*Important dates*

Draft paper submission:  July   31st, 2023
Draft paper notification:August  1st, 2023
Early registration deadline: August 11th, 2023
Late registration deadline:  August 23rd, 2023
Symposium:   August 29th - August 31st (3 days)
*Scope*

The goal of the IFL symposia is to bring together researchers actively
engaged in the implementation and application of functional and
function-based programming languages. IFL 2022 will be a venue for
researchers to present and discuss new ideas and concepts, work in
progress, and publication-ripe results related to the implementation
and application of functional languages and function-based
programming.

Topics of interest to IFL include, but are not limited to:

* language concepts
* type systems, type checking, type inferencing
* compilation techniques
* staged compilation
* run-time function specialization
* run-time code generation
* partial evaluation
* abstract interpretation
* metaprogramming
* generic programming
* automatic program generation
* array processing
* concurrent/parallel programming
* concurrent/parallel program execution
* embedded systems
* web applications
* embedded domain specific languages
* security
* novel memory management techniques
* run-time profiling performance measurements
* debugging and tracing
* virtual/abstract machine architectures
* validation, verification of functional programs
* tools and programming techniques
* industrial applications
*Submissions and peer-review
*
Following IFL tradition, IFL 2023 will use a post-symposium review
process to produce the formal proceedings.

Before the symposium authors submit draft papers. These draft papers
will be screened by the program chair to make sure that they are
within the scope of IFL. The draft papers will be made available to
all participants at the symposium. Each draft paper is presented by
one of the authors at the symposium. Notice that it is a requirement
that accepted draft papers are presented physically at the symposium.

After the symposium, a formal review process will take place,
conducted by the program committee.  Reviewing is single blind. There
will be at least 3 reviews per paper. The reviewers have 6 weeks to
write their reviews. For the camera-ready version the authors can make
minor revisions which are accepted without further reviewing.

Contributions submitted for the draft paper deadline must be between
two and twelve pages long. For submission details, please consult the
IFL 2023 website at 
https://urldefense.com/v3/__https://ifl23.github.io/__;!!IBzWLUs!TBCXTKguZVkN528s-avdxWSzUSEZDovNpLUUn2FpJ9WoV43bnCPWisFI8-77HuIIJyeD4PC3Fy2rQgxLc97z6bKtYocyMyGeCHxIBk4r$
 

.
*Where
*
IFL 2023 will be held physically in Braga, Portugal, arranged by
University of Minho.

See the IFL 2023 website at 
https://urldefense.com/v3/__https://ifl23.github.io/__;!!IBzWLUs!TBCXTKguZVkN528s-avdxWSzUSEZDovNpLUUn2FpJ9WoV43bnCPWisFI8-77HuIIJyeD4PC3Fy2rQgxLc97z6bKtYocyMyGeCHxIBk4r$
 

for more
information.

[image: beacon]

[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 ]

[Apologies for 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!XdwHWJXjXQPeHjKjBKwRUZi6oCg9AiohcetuEF_5FyUwiIGlYX3xaWdk1BLhzmT0NNg_Prbz8JKTfdOMX30ngPhhJl4$ 


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

- Martin Hutzler: TBA
- 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