The state of Illinois dissolved both AAR and CADE as corporations back in 1995. While CADE was re-established in the state of New York, this did not happen to AAR. Still, the AAR newsletter was continued and the member database kept up to date.
End of 2020 we started an initiative to revive AAR in order
To this end a zoom meeting with members of the current AAR board and representatives of automated reasoning conferences took place
Any comments on this initiative are highly welcome and may be send to Ulrich Furbach (AAR Vice President), Philipp Ruemmer (AAR Secretary) or any of the conference representatives
!!!! no later than two weeks after publication of this newsletter !!!!
A transition to a newly established AAR will be accomponied by a vote of the current members whether they want to join the newly established AAR.
The TPTP World Google group and Emailing list has been created to keep TPTP users informed of current developments in the TPTP World, and solicit feedback to guide future developments. (In the unlikely event that you have not heard of the TPTP World, it's time for you to visit the TPTP website!) If you would like to subscribe, please visit the google group web page.
An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see here, here and here.
The 2020 Alonzo Church Award was given jointly to Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, Lucian Popa, and Wang Chiew Tan for their ground-breaking work on laying the logical foundations for data exchange. Lists containing this and all previous winners can be found through the links above.
Eligibility and Nominations
The contribution must have appeared in a paper or papers published within
the past 25 years. Thus, for the 2021 award, the cut-off date is January 1,
1996. When a paper has appeared in a conference and then in a journal, the
date of the journal publication will determine the cut-off date. In
addition, the contribution must not yet have received recognition via a
major award, such as the Turing Award, the Kanellakis Award, or the Gödel
Prize. (The nominee(s) may have received such awards for other
contributions.) While the contribution can consist of conference or journal
papers, journal papers will be given a preference.
Nominations for the 2021 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness.
Nominations should be submitted to Javier Esparza by April 1, 2021.
Presentation of the Award
The 2021 award will be presented at the ACM SIGLOG/IEEE Symposium on
Logic in Computer Science, LICS 2021, which is scheduled to take place in Rome
in June/July 2021. The award will be accompanied by an invited lecture by the
award winner, or by one of the award winners. The awardee(s) will receive a
certificate and a cash prize of USD 2,000. If there are multiple awardees, this
amount will be shared.
Award Committee
The 2021 Alonzo Church Award Committee consists of the following five members:
Mariangiola Dezani, Thomas Eiter, Javier Esparza (chair), Radha Jagadeesan, and
Igor Walukiewicz.
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, with financial support of the E.W. Beth Foundation.
Nominations are now invited for the best dissertation in these areas resulting in a Ph.D. degree awarded in 2020.
The deadline for nominations is the 15th of April 2021.
Qualifications:
The prize consists of:
Only digital submissions are accepted, without exception. Hard copy submissions are not allowed. The following documents are to be submitted in the nomination dossier:
All pdf documents must be submitted electronically, as one zip file, via EasyChair. In case of any problems or questions please contact the chair of the committee Mehrnoosh Sadrzadeh.
The prize will be awarded by the chair of the FoLLI board at a ceremony during the 32nd ESSLLI summer school, which will be based in Utrecht, but held online August 2-13, 2021.
Beth dissertation prize committee 2021:
FoLLI is committed to diversity and inclusion and we welcome dissertations from all under-represented groups.
Nominations are now invited for the 2021 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2019 and 31 December 2020 are eligible for nomination for the award.
The deadline for submission is 1 July 2021. Submission details follow below.
Nominations can be submitted from 1 March 2021 and should be sent to the chair of the Jury, Thomas Schwentick
The Award
The 2021 Ackermann award will be presented to the recipient(s) at CSL
2022, the annual conference of the EACSL.
The award consists of
The jury is entitled to give the award to more (or less) than one dissertation in a year.
The Jury
The jury consists of:
How to submit The candidate or his/her supervisor should submit
SAT 2021 welcomes scientific contributions addressing different aspects of the satisfiability problem, interpreted in a broad sense. Domains include MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), as well as Constraint Satisfaction Problems (CSP). Topics include, but are not restricted to: Theoretical advances; Practical search algorithms; Knowledge compilation; Implementation-level details of SAT solving tools and SAT-based systems; Problem encodings and reformulations; Applications; Case studies and reports on insightful findings based on rigorous experimentation.
Important Dates
For more information, see the conference's website.
Systems and applications incorporating Knowledge Representation and Reasoning (KR) have made tremendous progress over the last decades and become more and more pervasive in scientific, industrial and everyday life. Popular knowledge representation formalisms range from databases, ontologies, classical, probabilistic and non-monotonic logics to natural language, offering rich means to describe a variety of static as well as dynamic phenomena. Automated reasoning systems harness machine learning, combinatorial search and optimization methods, planning, proving, design and diagnosis techniques to provide powerful tools for analyzing and deriving conclusions from complex input data. Novel, general and interdisciplinary approaches are thus vital contributions at the intersection of science, industry and society, aiming to enhance the capabilities and outreach of KR principles and technologies.
We welcome papers on a wide range of topics, including classic KR tools/techniques as well as their usage for solving or supporting tasks in a range of areas, for example:
Important Dates
For more information, see the conference's website.
If the pandemic means that travelling is still an issue in October, we might change the plan and host the conference online.
ATVA 2021 is the 19th in a series of symposia aimed at bringing together academics, industrial researchers and practitioners in the area of theoretical and practical aspects of automated analysis, synthesis, and verification of hardware, software, and machine learning (ML) systems.
ATVA solicits high-quality submissions in the following suggestive list of topics:
Important Dates
For more information, see the symposium's website.
TABLEAUX is the main international conference at which research on all aspects -- theoretical foundations, implementation techniques, systems development and applications -- of tableaux-based reasoning and related methods is presented. The first TABLEAUX conference was held in Lautenbach near Karlsruhe, Germany, in 1992. Since then it has been organised on an annual basis (sometimes as a part of IJCAR).
Tableaux and other proof based methods offer convenient and flexible tools for automated reasoning for both classical and non-classical logics. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis.
Topics of interest include but are not limited to:
Important Dates
For more information, see the conference's website.
For more information, see the symposium's website.
Static analysis is widely recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area.
Important Dates All deadlines are AoE (Anywhere on Earth).
For more information, see the symposium's website.
FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis.
List of Topics
Topics of interest for FroCoS 2021 include (but are not restricted to):
Important Dates
Covid Statement
TABLEAUX 2021 and FroCoS 2021 are intended to be hybrid conferences welcoming
both physical and virtual participation. The organisers are closely monitoring
the pandemic situation and may choose to make the conference virtual-only if it
seems unreasonable to host any sort of physical event. A final decision will be
taken before 14 June (12 weeks before the conference) to leave ample time for
potential travel plans to be made.
For more information, see the symposium's website.
FM 2021 is the 24th international symposium in a series organised by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The symposia have been notably successful in bringing together researchers and industrial users around a programme of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral work. FM 2021 will be both an occasion to celebrate and a platform for enthusiastic researchers and practitioners from a diversity of backgrounds to exchange their ideas and share their experience.
FM 2021 will highlight the development and application of formal methods in a wide range of domains including software, cyber-physical systems and integrated computer-based systems. We are in particular interested in the application of formal methods in the areas of systems-of-systems, security, artificial intelligence, human-computer interaction, manufacturing, sustainability, power, transport, smart cities, healthcare, biology. We also welcome papers on experiences from application of formal methods in industry, and on the design and validation of formal methods tools.
We are monitoring closely the COVID-19 situation and, although we hope for an in-person event, we are also planning carefully for a virtual event or a hybrid virtual/person event, in case there will be travel restrictions or health advisories following the global Covid-19 crisis. We will announce a decision on the nature of the meeting in due course.
Topics of Interest
FM 2021 encourages submissions on formal methods in a wide range of
domains including software, computer-based systems,
systems-of-systems, cyber-physical systems, security, human-computer
interaction, manufacturing, sustainability, energy, transport, smart
cities, and healthcare. We particularly welcome papers on techniques,
tools and experiences in interdisciplinary settings. We also welcome
papers on experiences of formal methods in industry, and on the design
and validation of formal methods tools. The broad topics of interest
for FM 2021 include, but are not limited to:
Important Dates
For more information, see the symposium's website.
The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress. Formal proceedings are produced only after the symposium so that authors can incorporate this feedback in the published papers.
Topics of interest cover all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large, including, but not limited to:
Important Dates
For more information, see the symposium's website.
Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to:
Tracks and Special Sessions
Besides the main track, ICLP 2021 will host additional tracks:
Important Dates
For more information, see the conference's website.
Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.
Topics
Dates
For more information, see the conference's website.
The conference will be held in an in-person/virtual hybrid format at Yale University, USA, possibly transitioning to fully virtual depending on the COVID-19 situation.
FMCAD 2021 is the twenty-first in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
Topics of Interest
FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer- aided design. Topics of interest include (but are not limited to):
Important Dates
For more information, see the conference's website.
We hope to have a (hybrid) physical event, but presentations can be given remotely
The ICTAC conference series aims at bringing together researchers and practitioners from academia, industry and government to present research and exchange ideas and experience addressing challenges in both theoretical aspects of computing and the exploitation of theory through methods and tools for system development. ICTAC also aims to promote research cooperation between developing and industrial countries.
The conference concerns all aspect of theoretical computer science, including, but not limited to:
Important dates:
For more information, see the colloquium's website.
The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
Topics of interest include (but are not limited to):
Concerning the COVID-19 Pandemic:
Due the pandemic situation, the organization committee of QONFEST 2021 decided that all conferences will take place online.
Important Dates
For more information, see the conference's website.
Since 1994, the RAMiCS conference series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond.
RAMiCS 2021 will take place at CIRM, the Centre International de Rencontres Mathématiques at the beautiful Luminy campus close to Marseille. Depending on the Covid-19 situation, it will take the form of a physical conference, a virtual conference, or a hybrid between the two. There will be no inscriptions fees to the conference. A limited number of grants, covering lodging and catering, are supplied by CIRM and the Archimède Institute.
Topics: We invite submissions in the general fields of algebras relevant to computer science and applications of such algebras. Topics include but are not limited to:
Important Dates:
For more information, see the conference's website.
Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of algebraic objects etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis.
Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems which interact with humans naturally by reasoning, aiming at learning at scale.
The purpose of SCSS 2021 is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with modern artificial intelligence techniques.
Scope
SCSS 2021 solicits submissions on all aspects of symbolic computation
and their applications in software science, in combination with
artificial intelligence and cognitive computing techniques. The topics
of the symposium include, but are not limited to the following:
Important Dates
For more information, see the symposium's website.
The aim of GandALF 2021 is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization. Papers focused on formal methods are especially welcome. Authors are invited to submit original research or tool papers on all relevant topics in these areas. Papers discussing new ideas that are at an early stage of development are also welcome. The topics covered by the conference include, but are not limited to, the following:
Important Dates (all dates are AoE)
For more information, see the conference's website.
The 4th International Conference on Logic and Argumentation (CLAR 2021) invites contributions from logic, artificial intelligence, philosophy, computer science, linguistics, law, and other areas studying logic and formal argumentation.
The CLAR 2021 conference will highlight recent advances in logic and argumentation and foster interaction between these areas within and outside China.
List of Topics
Suggested topics include, but are not limited to the following:
Important Dates
For more information, see the conference's website.
Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.
Currently, we expect that the conference will be organized in a hybrid way: both with an in-presence component and an online component.
List of topics:
Important dates:
For more information, see the conference's website.
The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from the different communities interested in termination (e.g., working on computational mechanisms, programming languages, software engineering, constraint solving, etc.). The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications.
Topics:
The 17th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating
applications of termination (for example in complexity analysis,
program analysis and transformation, theorem proving, program
correctness, modeling computational systems, etc.) are very welcome.
Topics of interest include (but are not limited to):
Important Dates:
For more information, see the workshop's website.
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 2021 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
LFMTP 2021 will hold a special session in honour of Frank Pfenning.
Important Dates
For more information, see the workshop's website.
The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms.
The progress in computer-aided reasoning, both automatic and interactive, during the past decades, has made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and collaboration of the HOL Light and Isabelle systems in the formal proof of the Kepler conjecture.
Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools for exchanging problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation, and communication methods, standards, protocols, and programming interfaces. The workshop welcomes developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. We are interested both in success stories and descriptions of current bottlenecks and proposals for improvement.
Topics
Topics of interest for this workshop include all aspects of
cooperation between reasoning tools, whether automatic or interactive.
More specifically, some suggested topics are:
Important Dates
For more information, see the workshop's website.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems.
Topics of interest include:
Important Dates
For more information, see the workshop's website.
The goal of this workshop is to bring together researchers working on the theory, practice, and application of parallel and distributed automated reasoning. Whilst parallel and distributed computational resources have become more widely abundant, and utilised in many areas of computer science, the area of automated reasoning has not embraced this as fully. Through this workshop we aim to provide a platform for researchers to present and discuss solutions and challenges when considering the parallel or distributed execution of automated reasoners, including those from the fields of CP, SAT, SMT, ASP, (first-order and higher-order) ATP, and CHC, including the full range of algorithmic approaches. The aim is to create a broad forum that allows the cross-fertilisation of ideas e.g. allowing ideas from parallel SAT solving to inspire ATP techniques, or vice-versa.
The workshop is interested in theoretical frameworks, practical implementations, experimental studies, and applications of parallel or distributed reasoning. Relevant parallel or distributed approaches may include (but are not limited to):
Important dates
For more information, see the workshop's website.
What are the current challenges, applications, directions, or exemplary achievements of Automated Reasoning? Input from our community raised exciting topics including the following:
The main goal of this workshop is to bring together key people from various subcommunities of automated reasoning---such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving---to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community.
Important Dates:
For more information, see the workshop's website.
Unification is concerned with the problem of identifying given (first- or higher-order) terms, either syntactically or modulo a theory. It is a fundamental technique that is employed in various areas of Computer Science and Mathematics. In particular, unification algorithms are key components in completion of term rewriting systems, resolution-based theorem proving, and logic programming. But unification is, for example, also investigated in the context of natural language processing, program analysis, types, modal logics, and in knowledge representation.
UNIF 2021 is the 35th in a series of annual workshops on unification and related topics. Just as it predecessors', the purpose of UNIF 2021 is to bring together researchers interested in unification theory and its applications, as well as closely related topics, such as matching (i.e., one-sided unification), anti-unification (i.e., the dual problem to unification), disunification (i.e., solving equations and inequations) and the admissibility problem (which generalizes unification in modal logics). It will provide a forum for presenting recent (even unfinished) work, and discuss new ideas and trends in this and related fields.
IMPORTANT DATES:
For more information, see the workshop's website.
The 10th International Workshop on Confluence (IWC 2021) aims at promoting further research in confluence and related properties. Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties.
Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool supports, certification as well as new applications.
Topics
The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. IWC 2020 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research.
Important Dates
For more information, see the workshop's website.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and computational languages, supporting tool development and reasoning. The LSFA series' objective is to put together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side.
LSFA topics of interest include, but are not limited to:
Important dates
For more information, see the workshop's website.
The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.
List of Topics
Important Dates
For more information, see the workshop's website.
Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.
The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory.
Abstract submission deadline: May 25, 2021
For more information, see the workshop's website.
Interaction and Concurrency Experience (ICE) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for complex interactions.
The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models.
We solicit contributions relevant to Interaction and Concurrency, including but not limited to:
Important Dates
For more information, see the workshop's website.
The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:
Important Dates
For more information, see the workshop's website.
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 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 presentation and discussions, supplemented with invited talks.
Relevant subject matter includes but is not limited to:
Important dates:
For more information, see the workshop's website.
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-seventh WoLLIC will be held online from October 5 to 8, 2021. It is scientifically 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), ACM Special Interest Group on Logic and Computation (ACM-SIGLOG) (TBC), the Sociedade Brasileira de Computação (SBC), and the Sociedade Brasileira de Lógica (SBL).
Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are:
Important Dates
For more information, see the workshop's website.
The DL workshop is the major annual event of the description logic research community. It is the forum in which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences.
Scope
We invite contributions on all aspects of description logics, including,
but not limited to:
Important Dates
For more information, see the workshop's website.
The Student Session is a forum for PhD and Master students to present their research at the interfaces of logic, language and computation. It features three tracks: Logic & Computation (LoCo), Logic & Language (LoLa), and Language & Computation (LaCo).
We invite submissions of original, unpublished work from students in any area at the intersection of Logic & Language, Language & Computation, or Logic & Computation. Submissions will be reviewed by several experts in the field, and accepted papers will be presented orally. Selected papers will appear in the Student Session proceedings by Springer. This is an excellent opportunity to receive valuable feedback from expert readers and to present your work to a diverse audience.
Important Dates
Please take note of the following important dates:
For more information, see the school's website.
The annual Midlands Graduate School in the Foundations of Computing Science (MGS) offers an intensive programme of lectures on the mathematical foundations of computing. It addresses first of all PhD students in their first or second year, but is open to anyone interested in its topics, from academia to industry and around the world. The MGS has been run since 1999 and is hosted alternately by the Universities of Birmingham, Leicester, Nottingham and Sheffield. MGS 21 is its 21st incarnation. Information about previous events can be found at the MGS web site.
Registration
Participation at MGS 21 is free of charge, but selective. Requests
must be submitted online
Registration deadline is April 1.
Check out the program at the school's website.
In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-28 will be held on 13th July 2021, during the 28th International Conference on Automated Deduction (CADE-28). Details are available starting from ... here! (Some details of the LTB division are still to be finalized, hopefully soon.)
Registration for CASC-28 is now open. This year's T-shirt design surpasses all others ... don't miss out ... register today!
CoCo 2021 will run live during IWC 2021, the 10th International Workshop on Confluence, which is held virtually on July 23 as part of FSCD.
Problems submitted by June 10, 2021 (via the COPS web interface) will be considered for CoCo 2021. In addition, there is the option to submit secret problems after the tool submission deadline.
All competition categories in CoCo 2020 will run in 2021. Further details can be found here.
We are looking for postdoctoral researchers and research assistants at the PhD level to work on computational logic and/or automata theory jointly at Technische Universität Kaiserslautern and Max-Planck Institute for Software Systems (MPI-SWS), which are located in Kaiserslautern, Germany. Research assistants at the PhD level will be funded for a standard duration of a PhD study at TUK (between 3-4 years). Postdoc researchers will initially be funded for two years with a possibility of extension of up to four years. The expected starting date is as soon as possible (not later than September 2021, but this is negotiable).
Successful applicants will help drive our effort in developing theories and/or implementations of logic and automata-theoretic toolbox. This could include, for example, the development of a string constraint solver, as well as applying them to several domains including web security, personalized online education, program repair, and verification of parameterized systems. Other possible topics could include computational complexity analysis of evaluating path-based queries over graph databases.
Ideally, applicants should have strong backgrounds in computer science (or related areas like mathematics) with experience in at least two of the following areas: logic, algorithms, programming language theory/implementation, formal language theory, concurrency theory, database theory, and formal verification.
Research environment: successful applicants will work within the Automated Reasoning Research Group at both TU Kaiserslautern and MPI-SWS led by Prof. Anthony W. Lin. They will be co-supervised by Prof. Rupak Majumdar, and have the opportunity to collaborate with Dr. Georg Zetzsche. The group enjoys close collaborations with colleagues in the UK (Oxford, Edinburgh, Birmingham, and London), Sweden (Uppsala), Taiwan (Taipei), China (Beijing), Australia (Melbourne, Canberra), Singapore, and Chile (Santiago), among others.
For informal enquiries, please contact Prof. Anthony Lin.
To apply, please send a CV and a research statement in an email to Mrs. Judith Stengel.
Early applications deadline is noon CEST 21 March 2021. Depending on the remaining positions available, further applications may still be considered.
Dominique Unruh and his group are searching for candidates who are enthusiastic about driving forward the field of formal verification of quantum cryptography, either from the theory side, tool side, or the quantum languages side.
For more information, see here (postdoc) and here (phd).
The Department of Mathematics and Computer Science (IMADA) at the University of Southern Denmark (SDU), Odense, invites applications for assistant and associate professor positions in Computer Science. We are flexible with respect to the starting date, but expect this to be in 2021 or early 2022.
Application deadline: 7 April 2021.
We are interested in applicants from all fields in Computer Science who can either strengthen or complement the current Computer Science research conducted at IMADA.
Fluency in English is required. Knowledge of Danish is not a prerequisite for application.
Link for application, including the call with full details: here
The application must include the following:
For more information, please contact Jacopo Mauro.
CertiK is a world-leading cybersecurity firm based in NYC that focuses on auditing smart contracts, blockchain platforms and system software. It was founded by prof. Ronghui Gu (Columbia) and prof. Zhong Shao (Yale), drawing on their research about formal verification.
In-house, CertiK is developing an operating system kernel (CertiKOS) and a certified compiler (DeepSEA), both of them verified using the Coq proof assistant. Together with commercial clients we are using both Coq and SMT-based tools to verify software written in Rust and Go. We are looking for interns to help take our work to the next level.
Available projects include: verifying hypervisors and programming language runtimes written in Rust; adding new language features, optimizations, or new verified backends to DeepSEA; building new formal verification tools for Go and Solidity; and more.
The internship is suitable for current master/phd students, or strong undergraduates looking for research experience. Because of the current Covid-19 epidemic, these positions are completely remote. You should be familiar with one of the following areas:
Formal verification using an interactive proof assistant (e.g. from reading the Software Foundations textbook or similar). [Preferred] Experience with non-trivial projects written in Coq. Proficient in Rust.
OR
Familiar with compiler implementation (e.g. from taking an Compilers class), and experience with functional programming (e.g. Ocaml, Gallina). [Preferred] Previous experience working on a compiler; or experience specifying programming languages using operational semantics; or experience working with WASM, LLVM, or EVM.
OR
Experience with SMT-based theorem proving systems (Z3, Boogie, Why3, etc) or model checkers. [Preferred] Previous experience building verification tools for programming languages.
Please send applications via this link.
Heriot-Watt University has established a reputation for world-class teaching and leading-edge, relevant research, which has made it one of the top UK universities for innovation, business and industry. To celebrate our 2021 bicentenary of pioneering research, we have set ourselves the target of recruiting one hundred outstanding research academics between 2018 and 2021.
As part of this prestigious programme, the School of Mathematical and Computer Sciences (MACS) welcomes applications for the posts of Assistant / Associate Professor / Professor in Computer Science. We particularly welcome applicants with expertise in either:
In addition, and as part of the School’s on-going plans to open new joint Mathematics-CS and Statistics-CS posts, we encourage applicants who have interdisciplinary training or experience linking one of the outlined CS priority areas and topics in Mathematics and Statistics (including, but not limited to, algebra and category theory, discrete mathematics and logic, financial risk, cyber risk, actuarial and statistical data science, statistical machine learning, Bayesian computational methods).
The School strongly encourages and supports the generation of industry impact from research, and we welcome candidates with experience of working in industry on AI, data science, robotics, autonomous systems, verification or security projects or a strong track record of collaborating with industrial partners.
Exceptional candidates possessing an extensive track record of internationally excellent research and leadership may be considered for appointment at Chair level; candidates interested in the position at Chair level should in the first instance contact the Head of School, Prof Beatrice Pelloni.
The School of Mathematical and Computer Sciences is committed to support family friendly work practices and part-time working options as part of our Athena Swan Bronze award. We especially encourage women and members of underrepresented groups to apply for this position. We welcome and will consider flexible working patterns e.g. part-time working and job share options.
About our team:
The Department of Computer Scienceis internationally renowned for its world-class research across a number of areas,
including artificial intelligence and machine learning, data integration, knowledge representation, visualization and analytics,
natural language processing, formal methods, logic, type theory, programming languages, parallel computation, human-computer
and human-robot interaction, and cybersecurity.
Jointly with University of Edinburgh, we host the center for doctoral training “Edinburgh Centre for Robotics” and the UK’s first National Robotarium, that together form a £129M joint venture, a center of excellence for AI research on an international scale, and a research and innovation hub with >150 staff and PhD students. In RCUK’s recent Grand Challenges Scheme: Trustworthy Autonomous Systems (TAS), our academics form core teams in 2 out of 7TAS nodes (each node is supported by a £3M research grant). The two nodes stand for“Trust” and “Governance” in Autonomous Systems. Our grant funding in this area has also grown through being awarded jointly with another school at HWU an EPSRC Industrial Strategy Challenge Strategy Fund for the Robotics Hub for Offshore Robotics for Certification of Assets (ORCA) worth £14.6M, which is one of the largest industrial strategy challenge funds awards in Scotland.
The department has strong collaboration with Industry. Since 2014, we have undertaken 107 projects with industrial partners, through our doctoral training centers (40 industrial partners), the ORCA hub (30 industrial partners), and the TAS nodes. Among our collaborators are Amazon Research, BP, Chevron, FiveAI, Horiba Mira, Imandra, Kawasaki, Kuka Robotics, Lloyds, Schlumberger, and many others.
For further information, please consult the university job portal. For informal discussions about the position or the department of Computer Science please contact Prof. Ekaterina Komendantskaya (Head of Computer Science). Alternatively, you may like to approach one of the members of the recruitment committee:
The ANR Research Project PPS (Probabilistic Programming Semantics, ANR-19-CE48-0014) described here offers two 12 month postdoc positions for the next academic year:
Our goal is to develop formal methods for probabilistic computing (semantics, type systems, logical frameworks for program verification, abstract machines ,etc.), building on the many connections between Proof Theory, Linear Algebra and the Theory of Programming Languages which arise within Linear Logic.
Acquaintance with probabilistic programming languages, their mathematical semantics and/or their implementation, is welcome but not mandatory, although we expect the applicant to be excited to work on this topic.
Interested persons should contact as soon as possible
briefly outlining their academic background and research interest and indicating if they have a preference as to the location (I2M or IRIF).As a second step, a complete application consisting of
The review of applications will begin on March 1st and continue until the position is filled. The positions are expected to start on October 1st 2021 at the latest.
A fully funded PhD position in the field of formal methods and reverse engineering is available at the Open University of The Netherlands. The project concerns a collaboration with Virginia Tech (US) and the prestigious DARPA research institute. We are interested in decompilation (retrieving source code from a binary) while maintaining a formal correctness proof that everything is sound. This will make bottom-up formal verification possible: applying formal verification to binaries, instead of to source code. If you have an interest in and affinity with one of the fields of formal methods, compilation, low-level assembly code or reverse-engineering, then you must certainly apply. Unique about the project is:
The project starts in April 2021. For more information, do not hesitate to contact dr. Freek Verbeek. Applications can be done by sending your CV and a short application letter indicating your interest in the project to the same e-mail address.
The University of Illinois at Chicago CS department is seeking recent PhD graduates or soon-to-be-graduates from historically underrepresented backgrounds for the Bridge to the Faculty program, a two-year postdoctoral fellowship that transitions into a tenure-track Assistant Professor position at the end of the fellowship. This is a university-level initiative with the ultimate aim of increasing faculty diversity at UIC. We’re looking for applicants in any area of computer science whose creative work/research, teaching and service will contribute to diversity and equal opportunity in higher education. We’re particularly interested in scholars with the potential to bring perspectives that come from a non-traditional educational background or an understanding of the experiences of groups historically underrepresented in computer science.
The position is available in the Fall 2021 semester and the initial term of employment will be for up to 24 months, with a dedicated faculty line for successful scholars to continue their tenure-track career at UIC. For more information and links to apply, see here. If you have any questions, please contact Associate Prof. Chris Kanich or the staff at the Bridge to the Faculty program.
A postdoctoral researcher is sought for a two-year position in computer science at Rice University to work with Professors Lydia Kavraki and Moshe Vardi on analysis techniques for deep neural networks (DNNs).
The impressive capabilities of deep neural networks have inspired system developers to use them in safety-critical cyber-physical control systems, such as autonomous vehicles and air traffic collision avoidance systems. For such applications it is imperative that the correctness of DNN systems be verified. Furthermore, it is desirable that such system be resistant to perturbations introduced by an adversary, or by inadvertent data corruption from system noise, domain shift, or broken sensors. Several recent incidents have underscored the need to better understand DNNs, and verify both their safety and security.
This project aims at developing techniques for analysis of DNNs by combining methods from formal methods, cyber-physical systems, and robotics. We are seeking candidates who have demonstrated ability to lead and/or work collaboratively in teams comprised of individuals of diverse backgrounds, skills, and perspectives.
Background: Applicants must hold a Ph.D. in Computer Science, Electrical & Computer Engineering, Robotics, or a related field. Required skills include excellent analytical skills, excellent software engineering skills, and excellent writing skills. Candidates with current expertise at the intersection of formal methods and robotics/cyber-physical systems will be given priority. This position is particularly suited for candidates who want to follow a career in academia.
About Rice University: As a leading research university with a distinctive commitment to education, Rice University aspires to path breaking research, unsurpassed teaching, and contributions to the betterment of our world. It seeks to fulfill this mission by cultivating a diverse community of learning and discovery that produces leaders across the spectrum of human endeavor. The George R. Brown School of Engineering ranks among the top 20 of undergraduate engineering programs (US News & World Report) and is strongly committed to nurturing the aspirations of faculty, staff and students in an inclusive environment. Rice University is an Equal Opportunity Employer with commitment to diversity at all levels and considers for employment qualified applicants without regard to race, color, religion, age, sex, sexual orientation, gender identity, national or ethnic origin, genetic information, disability, or protected veteran status. Rice University, a Tier 1 Research University, is located in the vibrant urban setting of Houston, TX, the fourth largest city in the U.S. Rice is ranked #16 in National Universities in the 2021 by "US News Best Colleges" and #1 for Quality of Life in the Princeton Review’s 2021 edition of "The Best 382 Colleges."
Interested applicants should contact Professor Lydia Kavraki and Professor Moshe Vardi and provide
The position is available immediately and applications will be accepted until this position is filled.
The Constraint Reasoning and Optimization Group led by Matti Järvisalo at the University of Helsinki has openings for postdoctoral researchers and exceptional PhD candidates
The Constraint Reasoning and Optimization Group (CoReO) led by Prof. Matti Järvisalo at the Department of Computer Science, University of Helsinki, Finland, has openings for postdoctoral researchers (and potentially also for exceptional PhD candidates).
Broadly speaking, we are looking for people with research experience and background in one or more of the following (or related) areas:
The positions are funded by two major research grants by Adacemy of Finland titled "Declarative Boolean Optimization: Pushing the Envelope" (2019-2023) and "Symbolic Reasoning for Formally Verified and Explainable AI" (2020-2022).
Salaries are competitive e.g. on the European scale.
For the postdoc positions, an early-career track record in PhD research is expected, proven by publications in internationally recognized key publications venues and potentially by implementations of declarative solvers. Expertise in partical solver development, application-oriented studies, and theoretical analysis is equally appreciated.
Helsinki is a great city to work and live in (see here and here) and is the capital of Finland, a country that has a strong track record in general well-being, equality, and quality of life (see here). Finland is a modern, safe, and technologically advanced country, and a member of the EU and the eurozone.
To apply for the position, please contact Matti via email with your CV, publication list, and a short motivation letter explaining your background, research experience and interests, and motivations for applying for the position. Similarly, contact Matti by email in case you have further questions on the positions.
Review of applications will start immediately, and the position(s) will remain open until filled.
(First Posted: January 10, 2021)
Supervisors: - Prof. Barteld Kooi - Prof. Jorge A. Pérez
We seek excellent candidates for one four-year PhD scholarship on the topics of message-passing concurrency, modal logic, and type systems.
The PhD scholarship concerns the interdisciplinary project "Knowledge is Power: Reliable Communicating Software by Epistemic Logics", supported by the Young Academy Groningen .
Details on the PhD Scholarship program can be found here.
The starting point of the proposed research is "propositions as sessions", a remarkable principle that connects concurrency and logic in the style of the well-known Curry-Howard correspondence. In this project, you will enhance the expressiveness of analysis techniques for message-passing programs by incorporating forms of knowledge and belief in formal specifications of communicating programs. To this end, you will develop new extensions of "propositions as sessions" by exploiting elements from epistemic logics and modal logics.
Qualifications
You have an MSc degree (or equivalent) in Computer Science,
(Philosophical) Logic, Mathematics, or Artificial Intelligence, with
proven experience in at least two of the following:
Application
Details on the application procedure will be made available shortly here
You will be asked to provide the following documents:
Additional Information
Prospective applicants are strongly encouraged to contact the
supervisors for further details on the research project and also
advice on how to prepare their applications:
VERIMAG, a leading academic research laboratory, co-operated by the University of Grenoble and the National center for scientific research (CNRS), proposes two industrially-funded (CIFRE) positions :
In both cases, the candidate is to be hired on a 3-year contract by the industry partner, and will spend half time in the academic laboratory, half time in industry.
These topics and related areas are also available as regular PhDs, but then the candidate will need to apply for a 3-year scholarship, granted on a competitive basis.
Contact David Monniaux for more information.
The Security & Privacy group at TU Wien is currently looking for outstanding PhD candidates to conduct cutting edge research in
Successful candidates will join the newly established SecInt doctoral school at TU Wien and will have the opportunity to engage in research collaborations within the Vienna Security and Privacy Research Center. TU Wien offers an outstanding research environment and numerous professional development opportunities. The Faculty of Informatics is the largest one in Austria and is consistently ranked among the best in Europe. Finally, Vienna has been consistently ranked by Mercer over the last years the best city for quality of life worldwide.
The employment is full-time (40 hrs/week) and the salary is internationally competitive (the yearly entry-level gross salary is approx. 41.000 EUR, which roughly corresponds to 2.400 EUR net per month).
Interested candidates should send at their earliest convenience
The working language in the group is English, knowledge of German is not required.
The Research Assistant will work under the EPSRC Established Career Fellowship Project, POST: Protocols, Observabilities and Session Types.
Imperial College London provides a flexible arrangement to be able to start and work remotely until we reopen the campus. It is also flexible for the starting date.
Please contact Nobuko Yoshida, Imperial College London if you would like to apply to the position to have informal discussions.
Details here.
The project has particular emphasis on putting theory into practice, by embedding session types in a range of programming languages and applying them to case studies; or developing the links between session types and other areas of theoretical computer science. The research programme includes collaboration with several companies and organisations.
Candidates for the postdoc position will need to have expertise in either:
Different positions will be suitable for different points on the theory/practice spectrum. We are especially interested in candidates with a combination of theoretical and practical skills.
For more details, see here.
The focus of Imperial College London Group is theories and applications of (Multiparty) Session Types which include:
The contact person is Professor Nobuko Yoshida, Imperial College London.
Closing date: 29th March 2021, please contact Nobuko Yoshida earlier if you would like to apply to the position even if you wish to start later.
Robert Krebbers has an opening for a 4 year PhD position at Radboud University. In case of an exceptionally strong candidate, the PhD position can be turned into a postdoc position for 1.5 to 2 years.
The project involves the development of automatic methods for program verification based on concurrent separation logic and type systems. You will apply the developed methods to verify security and correctness properties of a realistic hypervisor written in C, as part of an ongoing collaborative project with Google, MPI-SWS, Cambridge, SNU, and Aarhus.
The foundations of this project will be developed on top of the Iris framework for concurrent separation logic in the Coq proof assistant. Iris has been developed over the last 5 years in collaboration with MPI-SWS and Aarhus, and has been used by (and received many contributions from) a large network of other institutes (including Boston College, Inria, CNRS, KU Leuven, ITU, UIC, CMU, MIT, and BedRock Systems). See here for the many projects and papers that involve Iris.
Requirements:
You have a strong background in programming language theory and formal verification. You like to work on deep foundational research, and apply your research to verification of real-life software. You are required to have a master's degree (or equivalent) in computer science or mathematics (or you expect to obtain such a degree soon). Prior knowledge of Coq is preferred.
Application:
Robert Krebbers will be considering applications until the position is filled (applications before April 1 are preferred). To apply for the position, please send a resume, grade transcript, motivation letter and research statement by email.
If you have questions, do not hesitate to contact him.
Employment conditions:
Radboud University offers an attractive salary (the gross salary of a PhD student starts at 2.395 EUR per month, and increases to 3.061 EUR per month in the last year, based on a 38-hour working week) and excellent employment conditions (including 8% holiday allowance, 8% end-of-year bonus, assistance with family-related support such as child care). See here for more information.
The starting date is flexible, but preferably as soon as possible.
The Department of Computer Science at University of Sheffield has an open position of Lecturer in Verification. Details can be found here.
Deadline March 29, 2021
Female applicants are particularly encouraged.
To strengthen its research capacity in newly emerging research fields in theoretical philosophy, the department of philosophy and religious studies at Utrecht University is currently looking for a PhD-student in one of the following areas:
The PhD position (4 years) is independent of any overarching research project and is funded by the Department of Philosophy and Religious Studies at Utrecht University. We ask prospective candidates to write a brief proposal fitting in with one of these themes.
Deadline for applications is April 25, 2021. Interviews will be scheduled for the week of May 17. Employment will become effective in September 2021.
For further information, please visit here.
Are you interested in publishing your AI research and, at the same time, helping to turn them into features of products used by many leading companies? Are you interested in working near Paris?
IBM Research is setting up a new team at the IBM Artificial Intelligence Co-Innovation Center in Paris-Saclay. It will be dedicated to the development of safe, explainable and responsible AI systems utilizing knowledge-based and data-driven AI techniques. The new team will work with IBM?s global Research team and will be co-located with the French software development teams in charge of IBM business rules, decision automation and decision optimization products. IBM Research is hiring Research Scientists interested in solving problems related but not limited to the following:
Required skills:
Interested? Please send your application to Anika Schumann.
The Tsinghua University - University of Amsterdam Joint Research Centre for Logic is looking for a postdoc in the field of logic, who can substantially contribute to research and teaching of the logic group in the department of philosophy. In research, the specific research topic will depend on the candidate's expertise. As regards teaching, the position imposes no obligation of teaching, but a broad and strong teaching competence will be very helpful.
The candidate needs to apply for the Shuimu Scholar Postdoc Program in Tsinghua University. Please read the details of the Program and contact Professor Fenrong Liu.
Shuimu Tsinghua Scholar Program's Global Recruitment
To attract excellent junior scholars to undertake research in Tsinghua
University, support their academic career, and educate leading researchers
in various fields, Tsinghua University has set up the Shuimu Tsinghua Scholar Program. The application and selection of the Shuimu Tsinghua Scholar Program for 2021 has now started, covering 50 disciplines of
doctoral degrees.We welcome junior scholars who are committed to academic
research and who are keen on innovation to join the program.
1. Scale and Benefits
For the year of 2021, the program will support not more than 200
people. The annual salary is 300,000 RMB before tax for two years. Shuimu
Scholars will be provided with transitional housing on the campus or
provided with housing subsidies of 42,000 RMB per year, state-funded
housing subsidies of 12,000 RMB per year, as well as subsidies for
property management and heating. Shuimu Tsinghua Scholars enjoy the
privilege of the medical plan as Tsinghua faculty, and their children have
the privilege of going to Tsinghua University's kindergarden and Tsinghua
University Primary School like the children of other Tsinghua teachers.
Shuimu Tsinghua Scholars can participate in career training courses
offered to Tsinghua faculty, and can apply for funds and allowances for
attending top-level international conferences.
2. Application Requirements
Applicants must fulfill the following
requirements: applicants must be under 35 years old; their PhD degree must
have been obtained within the last three years,and fresh graduates are
given priority in consideration; they must be recommended by the interview
of the department; they must undertake to work full time at Tsinghua
University after entering Tsinghua University.
Candidates will be reviewed in terms of their academic ability, their research plan, and the potential effect on the subject field, in addition to related overall factors.
3. Application Materials
Shuimu Tsinghua Scholar Program Application Form, PART I. Academic and scientific
research materials (a scanned original in PDF format); articles,
monographs, patents or awards representing the applicant's highest
academic level and scientific research achievements may be selected.Among
them: the full text should be provided for articles (acceptance letters
should be provided for unpublished papers); the cover, catalogue and
abstract should be provided for monographs; copies of certificates should
be provided for patents or awards. Please scan the above materials into
one PDF file and send it to the mailbox of the department to which you are
applying. 2-3 letters of recommendation (including your PhD advisor's
recommendation letter) should be sent by your referees directly to the
department's mail address. If your recommendation letter is sent as an
attachment, it must be signed by the referee (sender).
4. Timeline
First term of application and review:
5. Contact For contact details of the department's coordinators, please refer to the website for Tsinghua University postdocs Here,you will benefit from top-level academic teachers,you will find a brand-new start to your independent academic career,and you will be nourished by the culture of this top-tiered universityin the world. Welcome to the family of Shuimu Tsinghua Scholar Program. Make yourself a better person in a better Tsinghua!
Download the application form here.
Applications are invited for an 18 month postdoctoral position in the Logic group of Prof. George Metcalfe at the Mathematical Institute of the University of Bern, supported by the Swiss National Science Foundation project "Hidden Quantifiers".
Candidates are expected to have a PhD in Mathematics, Computer Science, or a related field, and have research experience in universal algebra, proof theory, or non-classical logics. Proficiency in written and spoken English is also required.
To apply please send a full CV and recent research paper to Prof. George Metcalfe by 31 March, 2021.
Informal inquiries by email are very welcome.
At the new campus of Lancaster University in Leipzig (Germany) we currently have two open positions for Lecturers and one open position for a Teaching Fellow, all in Computer Science.
The deadline for applications for these positions is the 7th of April.
Details can be found here: