[TYPES/announce] PhD positions in Mathematical Foundations of Computer Science - Bath - deadline 4 March
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are recruiting for 2 PhD positions Funding: Competition funded Deadline: Friday 4 March 2022 Start:October 2022 (anticipated) Contacts: Willem Heijltjesw.b.heijlt...@bath.ac.uk Alessio Guglielmi a.guglie...@bath.ac.uk Mathematical Foundations Group Department of Computer Science University of Bath = The Mathematical Foundations group = Our group explores some of the deepest topics in logic and their relation to the theory of computation. We establish bridges between proof theory, category theory, semantics and complexity, so that the methods of each discipline enrich the others. We design new theories and solve old problems. For example, we defined a new proof formalism, called 'open deduction', that allowed us to describe one of the most efficient known notions of computation for the lambda-calculus. That was made possible by introducing ideas from complexity theory and category theory into proof theory and its computational interpretations. Our research programme, in a nutshell, is to help develop the mathematics of computation. This matters at least for two reasons. The first is that computing, at present, is art, not engineering. Indeed, because of the lack of mathematics, software correctness is not guaranteed the same way a bridge is guaranteed to stand, for example. The second reason is that the theory of computation is rapidly becoming one of the most important intellectual achievements of civilisation. For example, it is now helping physics and biology create new models in their domain. Because of all that, our doctoral graduates have embarked on excellent academic careers in some of the most intellectually rewarding and innovative branches of research, and will continue to do so. Our webpage: https://urldefense.com/v3/__https://www.bath.ac.uk/projects/mathematical-foundations-of-computation/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3tywO-43g$ Please see at the end of this email for a list of projects and supervisors. = How to apply = To apply, please send a CV and transcript to one of the contacts: Willem Heijltjesw.b.heijlt...@bath.ac.uk Alessio Guglielmi a.guglie...@bath.ac.uk We recommended to contact us informally first, or to contact one of the supervisors of the projects at the end of this email. Please use the above contacts also for any questions. Applicants should hold, or expect to gain, a First Class or good Upper Second Class Honours degree in Mathematics or Computer Science, or the equivalent from an overseas university. A Master’s level qualification would be advantageous. Non-UK applicants will also be required to have met the English language entry requirements of the University of Bath: https://urldefense.com/v3/__http://www.bath.ac.uk/corporate-information/postgraduate-english-language-requirements-for-international-students/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3sA8_Jw0A$ Anticipated start date: Monday 3 October 2022 = Funding = Candidates applying for this project may be considered for a 3.5-year studentship from the Engineering and Physical Sciences Council (EPSRC DTP). Funding covers tuition fees, a stipend (£15,609 per annum, 2021/22 rate) and research/training expenses (£1,000 per annum). EPSRC DTP studentships are open to Home students, and a limited number of opportunities are available to excellent International candidates. = Projects and Supervisors = VERIFICATION FOR REAL POLYNOMIAL ARITHMETIC Russell Bradford | r.j.bradf...@bath.ac.uk | https://urldefense.com/v3/__http://people.bath.ac.uk/masrjb/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3uOsAYPAA$ James Davenport | j.h.davenp...@bath.ac.uk | https://urldefense.com/v3/__http://people.bath.ac.uk/masjhd/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3vY7opZDA$ Tom Powell| trj...@bath.ac.uk | https://urldefense.com/v3/__http://t-powell.github.io__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3spNE1KdA$ Many problems in building verified software systems in the real world (e.g. air traffic control) involve the proof of statements about real polynomial arithmetic, often including inequalities. In principle we have known how to solve such systems for many years, but the theoretical, and too often the practical, complexity is excessive. There has been much work, at Bath, Coventry and elsewhere, in reducing the cost for important special cases, notably the cases when there are equations as well as inequalities. However, this leads to a large piece of software, resting on fairly complicated theorems. Recent
[TYPES/announce] LSFA 2022 -- First Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] 17th Workshop on Logical and Semantic Frameworks with Applications - LSFA 2022 23-24 September 2022 https://urldefense.com/v3/__https://lsfa2022.dcc.ufmg.br/__;!!IBzWLUs!Hb5jKFdvHnb21Q-pz8xZGKSfLUvZtMNud98yGCAAYHgZokfexpgTJ826gz0v_lXqkVROOuQR09AkAg$ Belo Horizonte, Brazil First Call for Papers ***Overview*** 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. See lsfa.cic.unb.br for more information. LSFA topics of interest include, but are not limited to: * Automated deduction * Applications of logical and semantic frameworks * Computational and logical properties of semantic frameworks * Formal semantics of languages and systems * Implementation of logical and semantic frameworks * Lambda and combinatory calculi * Logical aspects of computational complexity * Logical frameworks * Process calculi * Proof theory * Semantic frameworks * Specification languages and meta-languages * Type theory ***Submissions*** Contributions should be written in English and submitted in full paper (with a maximum of 16 pages excluding references) or short papers (with a maximum of 6 pages excluding references). They must be unpublished and not submitted simultaneously for publication elsewhere. The papers should be prepared in LaTeX using the EPTCS style. The submission should be in the form of a PDF file uploaded to Easychair: https://urldefense.com/v3/__https://easychair.org/conferences/?conf=lsfa2022__;!!IBzWLUs!Hb5jKFdvHnb21Q-pz8xZGKSfLUvZtMNud98yGCAAYHgZokfexpgTJ826gz0v_lXqkVROOuT7zgdgVw$ The pre-proceedings, containing the reviewed papers, will be available at the LSFA's webpage. After the meeting, the authors will be invited to submit full versions of their works for the post-proceedings publication. At least one of the authors of each submission must register for the conference. Presentations should be in English. According to the submissions' quality, the chairs will promote the further publication of journal revised versions of the papers. Previous LSFA Special Issues have been published in journals such as The Logical J. of the IGPL, Theoretical Computer Science and Mathematical Structures in Computer Sciences (see the LSFA page https://urldefense.com/v3/__http://lsfa.cic.unb.br__;!!IBzWLUs!Hb5jKFdvHnb21Q-pz8xZGKSfLUvZtMNud98yGCAAYHgZokfexpgTJ826gz0v_lXqkVROOuSQ1kPXMw$ ). ***Important dates*** * Abstract: Monday 2 May * Submission: Monday 9 May * Notification: Saturday 9 July * Preliminary proceedings version due: Thursday 1 September * Conference: Friday-Saturday 23-24 September * Submission for final EPTCS proceedings: Monday 17 October * Final version: Monday 21 November ***Program Committee*** Beniamino Accattoli, Inria & École Polytechnique, France Sandra Alves, Universidade de Porto, Portugal Carlos Areces, Universidad Nacional de Córdoba, Argentina Mauricio Ayala Rincón, Universidade de Brasília, Brazil Haniel Barbosa, Universidade Federal de Minas Gerais, Brazil Mario R. Folhadela Benevides, Universidade Federal Fluminense, Brazil Alejandro Díaz-Caro, Universidad Nacional de Quilmes & ICC, CONICET/Universidad de Buenos Aires, Argentina Amy Felty, University of Ottawa, Canada Pascal Fontaine, University of Liège, Belgium (co-chair) Edward Hermann Haeusler, PUC-Rio de Janeiro, Brazil Delia Kesner, Université de Paris, France Temur Kutsia, RISC/Johannes Kepler University Linz, Austria Bruno Lopes, Universidade Federal Fluminense, Brazil Ian Mackie, Polytechnique, France, and University of Sussex, UK Alexandre Madeira, Universidade de Aveiro, Portugal Sérgio Marcelino, University of Lisbon, Portugal Mariano Moscato, National Institute of Aerospace, USA Daniele Nantes, Universidade de Brasília, Brazil (co-chair) Vivek Nigam, Huawei Munich Research Center, Germany Carlos Olarte, Université Sorbonne Paris Nord, France Mateus de Oliveira Oliveira, University of Bergen, Norway Valeria de Paiva, Topos Institute, Berkeley, USA, Brazil Alberto Pardo, Universidad de la República, Uruguay Elaine Pimentel, University College London, UK Giselle Reis, Carnegie Mellon University-Qatar, Qatar Umberto Rivieccio, Universidade Federal do Rio Grande do Norte, Brazil Camilo Rocha, Pontificia Universidad Javeriana - Cali, Colombia Daniel Ventura, Universidade Federal de Goiás, Brazil Petrucio Viana, Universidade Federal Fluminense, UFF, Brazil ***Organisers*** Haniel Barbosa (UFMG, Brazil) Mario S. Alvim (UFMG, Brazil) -- Daniele Nantes Grupo de Teoria da
[TYPES/announce] RC2022 final CFP [extended deadline]
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] === Final Call for Papers 14th Conference on Reversible Computation (RC 2022) https://urldefense.com/v3/__https://reversible-computation-2022.github.io/__;!!IBzWLUs!ClyCcYDDaWpRfZIzSVSGrWklJ6giWqjmfgSJxzE9k-2pcreSLswA2Nr-thazQ6pVK4ONZnvEuM5o_Q$ July 5th-6th, 2022, Urbino, Italy Abstract Submission: Mon, February 7th, 2022 Submission Deadline: Mon, February 21st, 2022 === ++ COVID-19 RC 2022 is planned as a physical, in-person event, with certain support for remote presence, both for speakers and for other participants who are unable or unwilling to come. Depending on the pandemic situation, we may have to cancel the physical event and adopt a fully remote solution ++ Reversible computation has a growing number of promising application areas such as low power design, coding/decoding, debugging, testing and verification, database recovery, discrete event simulation, reversible algorithms, reversible specification formalisms, reversible programming languages, process algebras, and the modeling of biochemical systems. Furthermore, reversible logic provides a basis for quantum computation with its applications, for example, in cryptography and in the development of highly efficient algorithms. First reversible circuits and quantum circuits have been implemented and are seen as promising alternatives to conventional CMOS technology. The conference will bring together researchers from computer science, mathematics, and physics to discuss new developments and directions for future research in Reversible Computation. This includes applications of reversibility in quantum computation. Research papers, tutorials, tool demonstrations, and work-in-progress reports are within the scope of the conference. Invited talks by leading international experts will complete the program. Contributions on all areas of Reversible Computation are welcome, including---but not limited to---the following topics: * Applications * Architectures * Algorithms * Bidirectional transformations * Circuit Design * Debugging * Fault Tolerance and Error Correction * Hardware * Information Theory * Physical Realizations * Programming Languages * Quantum Computation * Software * Synthesis * Theoretical Results * Testing * Verification = Important Dates = - Abstract Submission: Mon, February 28th, 2022 [extended] - Submission Deadline: Mon, February 28th, 2022 [extended] - Notification to Authors: Mon, April 4th, 2022 - Final Version: Mon, April 25th, 2022 - Conference: Tue-Wed, July 5th-6th, 2022 = Invited speakers = - Robert O'Callahan (rr debugger developer - Mozilla Foundation/Pernosco) - Vincent van Wingerden (Quantum Computing - Microsoft) = Paper submission = Interested researchers are invited to submit - full research papers (15 pages + 2 pages references), - tutorials (15 pages + 2 of bibliography), as well as - work-in-progress or tool demonstration papers (6 pages + 1 page references) in Springer LNCS format. 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. Contributions must be written in English and report on original, unpublished work, not submitted for publication elsewhere. Submissions not adhering to the specified constraints may be rejected without review. Each paper will undergo a peer review of at least 3 anonymous reviewers. All accepted papers will be included in the conference proceedings. Papers can be submitted electronically in PDF via the RC 2022 interface of the EasyChair system: https://urldefense.com/v3/__https://easychair.org/conferences/?conf=rc2022__;!!IBzWLUs!ClyCcYDDaWpRfZIzSVSGrWklJ6giWqjmfgSJxzE9k-2pcreSLswA2Nr-thazQ6pVK4ONZnvw3xhyHA$ SPECIAL ISSUE Selected papers will be invited to a special issue on the Journal of Logical and Algebraic Methods = Organizers = * Program co-chairs * Claudio Antares Mezzina University of Urbino, Italy Krzysztof Podlaski University of Łódź, Poland = Program Committee = Clément Aubert (Augusta University, US) Kamila Barylska (Nicolaus Copernicus University, Poland) Robert Glück (University of Copenhagen, Denmark) Ivan Lanese (University of Bologna/INRIA, Italy) Hernan Melgratti (ICC - Universidad de Buenos Aires / Conicet, Argentina) Keisuke Nakano (Tohoku University, Japan) Alexandru Paler (Aalto University, Finland) Iain Phillips (Imperial College, UK) G. Michele Pinna (University of Cagliari, Italy) Neil (Julien) Ross (Dalhousie University, Canada) Bruno Schmitt (EPFL, Switzerland) Harun Siljak (Trinity
