[TYPES/announce] Call for papers - ThEdu'21 post-proceedings at EPTCS
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Open Call for Papers ** Proceedings for ThEdu'21 Theorem Proving Components for Educational Software http://www.uc.pt/en/congressos/thedu/thedu21 ** to be published by EPTCS, Electronic Proceedings in Theoretical Computer Science http://published.eptcs.org ** Synopsis ThEdu'21, was accepted as a workshop at CADE28 The 28th International Conference on Automated Deduction, 11-16 July 2021. Because of the COVID-19 pandemic, CADE28 and all its workshops were virtual events. It was a very lively virtual meeting with an average of 18 attendees. ThEdu'21 programme comprised one invited talk, 11 regular contributions and one demonstration, whose abstracts, presentations and videos are in the workshop web-page. Now post-proceedings are planned to collect the contributions upgraded to full papers. The contributions' topics are diverse according to ThEdu's scope, and this is a call open for everyone, also those who did not participate in the workshop. All papers will undergo review according to EPTCS standards. ThEdu'21 Scope: 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. This volume of EPTCS intends to bring 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. Important Dates * Submission (Full Papers): 10 October 2021 * Notification of acceptance: 28 November 2021 * Revised papers due: 12 December 2021 Topics of interest include: * methods of automated deduction applied to checking students' input; * methods of automated deduction applied to prove post-conditions for particular problem solutions; * combinations of deduction and computation enabling systems to propose next steps; * automated provers specific for dynamic geometry systems; * proof and proving in mathematics education. Submission We welcome submission of full papers (12--20 pages) presenting original unpublished work which is not being submitted for publication elsewhere. All contributions will be reviewed (at least three blind reviews) to meet the high standards of EPTCS. The authors should comply with the "instructions for authors", LaTeX style files and accept the "Non-exclusive license to distribute" of EPTCS: Instructions for authors (http://info.eptcs.org/) LaTeX style file and formatting instructions (http://style.eptcs.org/) Copyright (http://copyright.eptcs.org/) Papers should be submitted via EasyChair, https://easychair.org/conferences/?conf=thedu21. Program Committee Francisco Botana, University of Vigo at Pontevedra, Spain David Cerna, Johannes Kepler University, Austria João Marcos, Universidade Federal do Rio Grande do Norte, Brazil (co-chair) Filip Maric, University of Belgrade, Serbia Adolfo Neto, Universidade Tecnológica Federal do Paraná, Brazil Walther Neuper, Graz University of Technology, Austria (co-chair) Pedro Quaresma, University of Coimbra, Portugal (co-chair) Philippe R. Richard, Université de Montréal, Canada Vanda Santos, University of Aveiro, Portugal Wolfgang Schreiner, Johannes Kepler University, Austria Jørgen Villadsen, Technical University of Denmark, Denmark
[TYPES/announce] Postdoc position: Formal Verification/Synthesis (Munich, Germany, deadline: August 28, 2021)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We invite applications for an EU funded post-doctoral researcher position in the field of formal verification/synthesis. The successful candidate is expected to advance the state of the art of abstraction-based synthesis and verification for nonlinear continuous-state plants and to extend existing synthesis software. Depending on background and interests of the candidate, possible research foci are: automated determination of error bounds for floating-point implementations of numerical algorithms; parallelizable on-the-fly synthesis algorithms; adaptive state discretization; input/output languages and compiler for synthesis software. Required qualifications: * PhD degree in Computer Science, Systems and Control, Mathematics, or a related field. Exceptionally qualified and experienced candidates with an MSc degree will also be considered. * Solid experience in one of the following fields: Set-valued numerics; validated floating-point arithmetic; dynamic programming; formal verification/synthesis; professional grade software development. * Programming proficiency (C or Ada). * Efficient communication skills in English. The position is full-time and paid according to pay scale ``TVOeD Bund, E 14''. Actual income depends on marital status and professional experience, and starts from EUR 33000 net p.a. (E-13/EUR 31000 for applicants with an MSc degree). Reimbursement for travel expenses to conferences. No teaching load. The position is available immediately and for a duration until April 2023. It is open to applicants worldwide; no special security clearance necessary. Your complete application consists of the following documents, which should be sent as a single PDF file to the email address given below (deadline: August 28, 2021): * CV * One-page cover letter (clearly indicating available start date as well as relevant qualifications, experience and motivation) * University certificates and transcripts (BSc, MSc and PhD degrees) * Up to three letters of recommendation * List of publications * Possibly an English language certificate All documents should be in English or German. Gunther Reissig http://www.reiszig.de/gunther/ Email: gunther2...@reiszig.de, Subject: Postdoc ref 9y22x Bundeswehr University Munich, Germany Department of Aerospace Engineering Institute of Control Engineering
[TYPES/announce] Postdoctoral Researcher at Cornell University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We invite applications for a postdoctoral research associate at Cornell University. The position is part of the Pronto Project (prontoproject.org). We are developing verified compilers for network devices. Applicants should have a PhD in Computer Science, expertise in programming languages design and implementation, strong communication skills, and a desire to work as part of an interdisciplinary team. A background in networking is not required. However, familiarity with formal semantics and proof assistants is preferred. The successful candidate will be provided with significant freedom to explore ideas that expand the scope of the project as well as opportunities for professional development. The position is for one year initially but may be extended to additional years. To apply, please send a CV, a research statement, one representative publication, and the names of three references to Nate Foster ( jnfos...@cs.cornell.edu). We especially welcome applications from women and members of under-represented minority groups.