[TYPES/announce] Call for papers - ThEdu'21 post-proceedings at EPTCS

2021-07-28 Thread Walther Neuper
[ 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)

2021-07-28 Thread Gunther Reißig

[ 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

2021-07-28 Thread Nate Foster
[ 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.