[TYPES/announce] PhD and post-doc positions in Mainz, Germany

2022-11-28 Thread Erdweg, Sebastian
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We have multiple open positions for PhD students and post-docs in the PL Group 
of
the University of Mainz in Germany. The available positions include a gross 
monthly
salary of ~4000 Euro. Our team meets and socializes in Mainz; remote work is an 
option.

The PL Group at the University of Mainz was founded in 2019. Our goal is to
support developers in creating and maintaining software systems that are easier
to write, more secure, run faster, and consume less energy. Our current research
topics include:

-- Incremental computing: How can a computation react to a change of its input
   efficiently? We have observed up to 10,000x speedups in prior work, can
   incrementality help us save as much energy? Can we build a new foundation for
   incremental computing to support a wider range of computations?
-- WebAssembly: How can we discover and prevent security vulnerabilities in
   WebAssembly? We have built a data-flow analysis platform for WebAssembly to
   identify properties of WebAssembly programs at compile time. Can this 
platform
   be used to protect WebAssembly users while also optimizing the code for
   performance?
-- Datalog: How can the power of Datalog best be exploited in modern software
   development? How can we abstract over and hide the technicalities of Datalog,
   for example, by compiling DSLs to Datalog. And how can we optimize Datalog 
code
   to provide truly declarative performance, without exposing users to details 
of
   the underlying database technology?
-- Language engineering: How can we build programming-language tools with modest
   effort and without duplicating the language's semantics? For example, can we
   derive type checkers, debuggers, and other editor services from the 
language’s
   semantics? And does this require a language workbench or can we support rich
   services for embedded languages as well?

Mainz is part of the Frankfurt Metropolitan Area and only a short train ride
away from Frankfurt's international community and culture. Mainz itself lies at
the confluence of the Rhine and Main rivers, surrounded by plenty of nature.
https://urldefense.com/v3/__https://mainz.de/en/worth-seeing/reasons-to-love-mainz.php__;!!IBzWLUs!Vg20rrpKTO1LE18FQ_3Sauc3RHj2z417izDJatQxpBFvwBTscaxIGwpXSgc-8A--sYoD64r9SOuJZ7veccxytaX4la1QJ0sBzg$
 

I'm excited to hear from interested candidates via email. If you know potential
candidates, please forward this message to them.

Sebastian Erdweg
https://urldefense.com/v3/__https://www.pl.informatik.uni-mainz.de/erdweg__;!!IBzWLUs!Vg20rrpKTO1LE18FQ_3Sauc3RHj2z417izDJatQxpBFvwBTscaxIGwpXSgc-8A--sYoD64r9SOuJZ7veccxytaX4la3bNuod-A$
 



[TYPES/announce] FSCD 2023: First Call for Papers

2022-11-28 Thread Carsten Fuhs

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

  CALL FOR PAPERS
 Eighth International Conference on
Formal Structures for Computation and Deduction (FSCD 2023)
July 3-6, 2023, Rome, Italy
https://urldefense.com/v3/__https://easyconferences.eu/fscd2023/__;!!IBzWLUs!WKzkX8GXPNruUEGQhunN41gqqVl7ZRCEhHkMykcb4jlC_iGhc21za8Q84YMB38R-2REp0vuBiuUWiBZQn7FdgZousz7DgWzLYFte$ 
 In-cooperation with ACM SIGLOG and SIGPLAN


IMPORTANT DATES
---
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not 
be considered.

Abstract:  January 30, 2023
Submission:February 3, 2023
Rebuttal:  March 24-28, 2023
Notification:  April 13, 2023
Final version: April 27, 2023

OVERVIEW

FSCD 
(https://urldefense.com/v3/__https://fscd-conference.org/__;!!IBzWLUs!WKzkX8GXPNruUEGQhunN41gqqVl7ZRCEhHkMykcb4jlC_iGhc21za8Q84YMB38R-2REp0vuBiuUWiBZQn7FdgZousz7Dgczxr8sv$
 ) covers all aspects of formal structures for computation and deduction from 
theoretical foundations to applications. Building on two communities, RTA 
(Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and 
Applications), FSCD embraces their core topics and broadens their scope to 
closely related areas in logic, models of computation, semantics and 
verification in new challenging areas.

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

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

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

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

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

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

6. Formal Systems for Semantics and Verification in new challenging areas:
 - Certification;
 - Security;
 - Blockchain protocols;
 - Data bases;
 - Deep learning and machine learning algorithms;
 - Planning.

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

SPECIAL ISSUE
-
We aim to have a special issue of Logical Methods in Computer Science of 
selected papers. More details will be provided later.


SUBMISSION GUIDELINES
-
The submission site is:

   https://urldefense.com/v3/__https://easychair.org/conferences/?conf=fscd2023__;!!IBzWLUs!WKzkX8GXPNruUEGQhunN41gqqVl7ZRCEhHkMykcb4jlC_iGhc21za8Q84YMB38R-2REp0vuBiuUWiBZQn7FdgZousz7DgTFT6JEU$ 


Submissions must be formatted using the LIPIcs style files 
(https://urldefense.com/v3/__https://submission.dagstuhl.de/series/details/5*author__;Iw!!IBzWLUs!WKzkX8GXPNruUEGQhunN41gqqVl7ZRCEhHkMykcb4jlC_iGhc21za8Q84YMB38R-2REp0vuBiuUWiBZQn7FdgZousz7DgQdGAjN-$
 ) and submitted via EasyChair.

Submissions can be made in two categories.  Regular research papers are limited 
to 15 pages, excluding references and appendices.  They must present original 
research which is unpublished and not submitted elsewhere.  System descriptions 
are limited to 15 pages, excluding references. Shorter papers are welcome and 
will be given equal consideration.
A system description must present new software tools, or significantly new 
versions of such tools, in which FSCD topics play an important role. An archive 
of the code with instructions on how to install and run the tool must be 
submitted.  In addition, a webpage where the system can be experimente

[TYPES/announce] 7 PhD positions available in Austria within the SPyCoDe (Semantic and Cryptographic Foundations of Security and Privacy by Compositional Design) Special Research Program

2022-11-28 Thread Maffei, Matteo
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

SPyCoDe (Semantic and Cryptographic Foundations of Security and Privacy by 
Compositional Design) is a special research program funded by FWF. World-class 
researchers from TU Wien, IST Austria, Universität Wien, TU Graz and 
Universität Klagenfurt team up to create the technological foundations for 
designing complex, multi-layer systems with provable S&P guarantees. 
Interdisciplinary approach integrates computer-aided verification, system 
security, cryptography, and touching on further fields, like networks, game 
theory, and blockchains. The team includes experts from all disciplines at the 
core of SPyCoDe, with 6 ERC grant holders (for a total of 10 ERC grants), 6 
young researchers who already received prestigious awards, and >40% female 
researchers.
SPyCoDe is looking for 7 highly qualified and motivated students who have a 
master's degree in computer science or another related field and experience in 
formal methods, system security, security and privacy and/or cryptography for 
collaborative interdisciplinary research. SPyCoDe is offering PhD positions for 
4 years for 30 hours/week, with an option to upgrade to 40 hours/week with very 
competitive salary.
The 7 projects available in this call are list below, along with the principal 
investigator acting as supervisor and the research institution:

№

Project Title


Principal Investigator

Research Institution

1

Interface Theory for Security and Privacy

Henzinger , Thomas A.

IST Austria


2

Game-Theoretic Models for Blockchain Applications

Fuchsbauer, Georg

TU Wien


5

Verification of Side Channel Properties

Bloem, Roderick

TU Graz


4

Cross-Layer Security for Blockchain Consensus

Pietrzak, Krzysztof

IST Austria

5

Security and Privacy by Design for Smart Contracts

Maffei, Matteo

TU Wien


6

Secure Blockchains in Network Transition Periods

Ullrich, Johanna

Universität Wien

7

Secure Network and Hardware for Efficient Blockchains

Kokoris-Kogias, Eleftherios

IST Austria




Application start: 28.11.2022
Application deadline:  23.12.2022
Expected start of work: 01.02.2023

You can find more information about the projects, requirements for candidates 
and application procedure on the SPyCoDe website 
https://urldefense.com/v3/__https://spycode.at__;!!IBzWLUs!Ug1zy62Qh-_anc49iS1lGS1lVqshVSLO09qlTVC8nBGarculcWb7a437xwQKCur1Wx8LFtxKyVrm3GQwgyIj9YZCiAV3tSMJNlV7dKk-E1M$
 









[TYPES/announce] Tenure-Track Faculty Position at Illinois Tech

2022-11-28 Thread Stefan Muller

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

Illinois Tech is hiring this year (for Fall 2023), and PL is likely to 
be one of a few focus areas. We have a close-knit, highly collaborative 
faculty and an excellent, diverse, and excited group of students, and 
are located in Chicago!


Application and more information are here: 
https://urldefense.com/v3/__https://academicjobsonline.org/ajo/jobs/23124__;!!IBzWLUs!WelIp5g__lse0RS9Iqv49Ip3iNnaxONHOhHGK26TKkJANioKRO_5WaFF2uHu5BH-b0ctaYSvNCmOpzLSi5AcOMoWjiMoZa6x$ 


Feel free to contact me (smull...@iit.edu) with any questions.

Stefan

--
Stefan Muller
Gladwin Development Chair Assistant Professor
Computer Science Department
Illinois Institute of Technology