[TYPES/announce] [fm-announcements] ITP 2017 - Final Call for Papers

[Munoz, Cesar (LARC-D320)]

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

   *** Apologies for multiple copies, please redistribute ***

 FINAL CALL FOR PAPERS

   ITP 2017
8th International Conference on Interactive Theorem Proving
  Brasilia, Brazil
   September 26-29, 2017
  http://itp2017.cic.unb.br


SUBMISSION DEADLINES
* April 3, 2017 (abstracts)
* April 10, 2017 (full papers)

GENERAL INFORMATION
The ITP conference series is concerned with all topics related to
interactive theorem proving, ranging from theoretical foundations to
implementation aspects and applications in program verification,
security, and formalization of mathematics. ITP is the evolution of
the TPHOLs conference series to the broad field of interactive theorem
proving. TPHOLs meetings took place every year from 1988 until
2009. The eighth ITP conference, ITP 2017, will be held at
Universidade de Brasilia, September 26-29, 2017.

SCOPE OF CONFERENCE
ITP welcomes submissions describing original research on all aspects
of interactive theorem proving and its applications. Suggested topics
include but are not limited to the following:

*  formal aspects of hardware and software
*  formalizations of mathematics
*  improvements in theorem prover technology
*  user interfaces for interactive theorem provers
*  formalizations of computational models
*  verification of security algorithms
*  use of theorem provers in education
*  industrial applications of interactive theorem provers
*  concise and elegant worked examples of formalizations (proof pearls)

PUBLICATION DETAILS
The proceedings of the symposium will be published in the
Springer's LNCS series.

** After the conference the authors of selected papers will be invited
to submit revised papers for a special issue of the Journal of Automated
Reasoning.  **

PAPER SUBMISSIONS
All submissions must be original, unpublished, and not submitted
concurrently for publication elsewhere. Furthermore, when appropriate,
submissions are expected to be accompanied by verifiable evidence of
a suitable implementation, such as the source files of a formalization
for the proof assistant used. Submissions should be no more than
16 pages in length and are to be submitted in PDF via EasyChair at
the following address:

   https://easychair.org/conferences/?conf=itp2017

Submissions must conform to the LNCS style in LaTeX. Authors of
accepted papers are expected to present their paper at the conference
and will be required to a sign copyright release form.

In addition to regular papers, described above, there will be a rough
diamond section. Rough diamond submissions are limited to 6 pages
and may consist of an extended abstract. They will be refereed and be
expected to present innovative and promising ideas, possibly in an
early form and without supporting evidence. Accepted diamonds will be
published in the main proceedings and will be presented as short
talks.

IMPORTANT DATES
Abstract submission deadline: April 3, 2017
Full paper submission deadline: April 10, 2017
Author notification:  June 2, 2017
Camera-ready papers:  June 30, 2017
Workshops & Tutorials:  September 23-25, 2017
Conference:  September 26-29, 2017

INVITED SPEAKERS
   Moa Johansson, Chalmers University of Technology, Sweden
   Leonardo de Moura, Microsoft Research
   Cezary Kaliszyk, Universitaet Innsbruck, Austria (joint with TABLEAUX and 
FroCos)
   Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and FroCos)
   Jasmin Blanchette, Inria and LORIA, Nancy, France (joint with TABLEAUX and 
FroCos)

WORKSHOPS AND TUTORIALS
   There will be a three-day programme of four workshops and four
   tutorials from 23-25 September.

   Workshops:
 12th Logical and Semantic Frameworks with Applications (LSFA 2017)
 Sandra Alves, Renata Wassermann, Flavio L. C. de Moura
 23 and 24 September 2017

 Proof eXchange for Theorem Proving (PxTP)
 Catherine Dubois, Bruno Woltzenlogel Paleo
 23 and 24 September 2017

 EPS - Encyclopedia of Proof Systems
 Giselle Reis, Bruno Woltzenlogel Paleo
 24 and 25 September 2017

 DaLi - Dynamic Logic: new trends and applications
 Mario Benevides, Alexandre Madeira
 24 September 2017

   Tutorials:

 General methods in proof theory for modal and substructural logics
 Bjoern Lellmann, Revantha Ramanayake
 23 September 2017

 From proof systems to complexity bounds
 Anupam Das
 24 September 2017

 Proof Compressions and the conjecture NP =3D PSPACE
 Lew Gordeev, Edward Hermann Haeusler
 25 September 2017

 PVS for Computer Scientists
 Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato
 25 September 2017

   Details will be published in separate calls and on the conference
   website.

PROGRAM COMMITTEE CHAIRS
Mauricio Ayala-Rincon, 

[TYPES/announce] Professor of Cyber Security at Kent

[Simon Thompson]

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


We’re looking to appoint a professor of Cyber Security at Kent, to head up our 
existing group, with its Masters course and research activities. The Cyber 
Security group also sits alongside our Programming Languages and Systems group, 
and someone with strengths in PL aspects of security would fit very well. 

The advert for a Professor of Cyber Security is live at 
https://jobs.kent.ac.uk/fe/tpl_kent01.asp?s=4A515F4E5A565B1A=40739,2141233446=49639912=824734655621=sesmvkldtcboaxhswn
 

and post has been advertised with an associated lectureship in security, so the 
successful candidate will have a chance to shape that appointment too.

If you’re interested, do think about applying, or get in touch with us. I’d be 
happy to answer emails, as would Richard Jones, head of school: cs-hos AT kent 
DOT ac DOT uk

Simon

Simon Thompson | Professor of Logic and Computation 
School of Computing | University of Kent | Canterbury, CT2 7NF, UK
s.j.thomp...@kent.ac.uk  | M +44 7986 085754 | 
W www.cs.kent.ac.uk/~sjt 

[TYPES/announce] TABLEAUX 2017 - Final Call for Papers

[Elaine Pimentel]

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

 FINAL CALL FOR PAPERS

   TABLEAUX 2017
 26th International Conference on Automated Reasoning with
   Analytic Tableaux and Related Methods
  University of Brasilia, Brazil
   September 25-28, 2017

   Deadlines: 18 Apr 2017 (abstract), 25 Apr 2017 (paper)

  http://tableaux2017.cic.unb.br/


GENERAL INFORMATION
  TABLEAUX is the main international conference at which research
  on all aspects, theoretical foundations, implementation techniques,
  systems development and applications, of the mechanization of
  tableau-based reasoning and related methods is presented. As
  the first TABLEAUX workshop was held in Lautenbach in 1992, this
  year's conference will include special events celebrating 25 years
  of TABLEAUX.

  The conference will be held in Brasilia from 25-28 September 2017.
  It will be co-located with both the 11th International Symposium
  on Frontiers of Combining Systems (FroCoS 2017) and the 8th
  International Conference on Interactive Theorem Proving (ITP
  2017).

TOPICS
  Tableau methods offer a convenient and flexible set of tools for
  automated reasoning in classical logic, extensions of classical
  logic, and a large number of non-classical logics. For large groups
  of logics, tableau methods can be generated automatically. 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:

* tableau methods for classical and non-classical logics
  (including first-order, higher-order, modal, temporal,
  description, hybrid, intuitionistic, substructural,
  relevance, non-monotonic logics) and their proof-theoretic
  foundations;
* related methods (SMT, model elimination, model checking,
  connection methods, resolution, BDDs, translation approaches);
* sequent calculi and natural deduction calculi for classical
  and non-classical logics, as tools for proof search and proof
  representation;
* flexible, easily extendable, light weight methods for theorem
  proving;
* novel types of calculi for theorem proving and verification
  in classical and non-classical logics;
* systems, tools, implementations, empirical evaluations and
  applications (provers, logical frameworks, model checkers, ...);
* implementation techniques (data structures, efficient
  algorithms, performance measurement, extensibility, ...);
* extensions of tableau procedures with conflict-driven
  learning, generation of proofs; compact (or humanly readable)
  representation of proofs;
* decision procedures, theoretically optimal procedures;
* applications of automated deduction to mathematics, software
  development, verification, deductive and temporal
  databases, knowledge representation, ontologies, fault
  diagnosis or teaching.

  We also welcome papers describing applications of tableau
  procedures to real world examples. Such papers should be tailored
  to the tableau community and should focus on the role of
  reasoning, and logical aspects of the solution.

CELEBRATING 25 YEARS
  To celebrate 25 years TABLEAUX the conference will include a
  special session of invited talks by:

  Reiner Haehnle   Technische Universitaet Darmstadt, Germany
  Wolfgang Bibel  Technische Universitaet Darmstadt, Germany

INVITED SPEAKERS:

  Carlos Areces  FaMAF - Universidad Nacional de Cordoba, Argentina
  Katalin Bimbo  University of Alberta, Canada  (with FroCoS and ITP)
  Jasmin Blanchette  Inria and LORIA, Nancy, France (with FroCoS and ITP)
  Cezary KaliszykUniversitaet Innsbruck, Austria (with FroCoS and ITP)

WORKSHOPS AND TUTORIALS
  There will be a three-day programme of four workshops and four
  tutorials from 23-25 September.

  Workshops:
12th Logical and Semantic Frameworks with Applications (LSFA 2017)
Sandra Alves, Renata Wassermann, Flavio L. C. de Moura
23 and 24 September 2017

Proof eXchange for Theorem Proving (PxTP)
Catherine Dubois, Bruno Woltzenlogel Paleo
23 and 24 September 2017

EPS - Encyclopedia of Proof Systems
Giselle Reis, Bruno Woltzenlogel Paleo
24 and 25 September 2017

DaLi - Dynamic Logic: new trends and applications
Mario Benevides, Alexandre Madeira
24 September 2017

  Tutorials:

General methods in proof theory for modal and substructural logics
Bjoern Lellmann, Revantha Ramanayake
23 September 2017

From proof systems to complexity bounds
Anupam Das
24 September 2017

Proof Compressions and the conjecture NP = PSPACE
Lew Gordeev, Edward Hermann Haeusler
25 September 2017

PVS for Computer Scientists

[TYPES/announce] Several positions (PhD/PostDoc) on security and formal modelling and/or programming for IoT and/or CPS in Oslo.

[Christian Johansen]

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

__

Several positions (PhD/PostDoc) on security and formal
modelling and/or programming for IoT and/or CPS.

Dept. of Computer Science, Univeristy of Oslo

See details at http://iotsec.no/phd
__


The University of Oslo (UiO) increases the focus on security and
formal methods applied to Internet of Things (IoT) and Cyber Physical
Systems (CPS). Several positions are opened on the topics:

*   Language-based Security and Analysis

*   Safety modelling and verification for IoT systems

*   Privacy and Security for Smart Environments

*   Security of Communication for IoT and Smart infrastructures

*   Fine-grained Access Control for e-Health Data


--
!!  Be aware that when you apply it is important to clearly mark which
!!  position(s) (and preference order) you are interested in.
--

===
General information
===

The PhD positions are related to both the IoTSec.no initiative and
the Strategic Research Initiative ConSeRNS, which is financed in part
by the Norwegian Research Council and the University of Oslo. You
will work together in a team with national project participants, and
international partners, as well as becoming part of the UiO working
and student environment.

The work will be conducted at UiO (Oslo) in Norway. You will be part
of an exciting arena for research and innovation, and have the
opportunity to work in an exciting international environment with
close contact to Research Institutes and Industry.

The PhD students will follow the traditional PhD education at UiO,
while there is also the possibility to take up a PhD in close
collaboration with an industry partner (Industrial PhD). All PhDs
require the admission to the PhD program of the University of Oslo.

Salary is after the rules from the state, based on your experience.


===
The application (Norwegian or English) should contain:
===

*   CV including names and contact information of two references
*   List of publications (if applicable)
*   Transcript of records for PhD applicants
*   Summary and status of your master thesis (or of PhD thesis in
case of Post-doc application)
*   A statement letter indicating your ideas and interests in one or
more of the above topics, and an indication if any other fields are
relevant for you.


===
Further information
===

For further information and application through e-mail, please
contact:

*   Olaf Owe, UiO/IFI, m: +47 22852449, o...@ifi.uio.no
*   Christian Johansen, UiO/ITS, m: +47 9753 5582, cri...@ifi.uio.no


=
Candidate profile
=

  The applicant is required to hold a Master's degree or equivalent in
computer science or mathematics and should have good analytical and/or
programming skills. The ideal candidate has background in one or more
of the areas covered by the above topic titles (see also link above).

  Besides technical skills, we are looking for a curious, ambitious
candidate who is highly motivated to do research and contribute to
the work done at our group. Good communication skills in both oral
and written English are expected. We strongly encourage that the
application is accompanied by a short cover letter explaining shortly
how the applicant's background and education fits to the goals and
requirements of the project(s)/group/topic.


=
Related links
=

IoTSec project: http://IoTSec.no,
More details at http://iotsec.no/phd
Institute for Informatics: http://ifi.uio.no
Doctoral education at the University of Oslo (UiO),
http://www.mn.uio.no/english/research/doctoral-degree-and-career/


==
Admission criteria for UiO
==

The purpose of the Ph.D. fellowship is research training leading to
the successful completion of a PhD degree. The fellowship requires
admission to the research training program at the Faculty of
Mathematics and Natural Sciences. Firstly, the applicants must have
obtained undergraduate (Cand.mag., i.e. B.Sc. level) with a level
corresponding at least "C" and postgraduate (cand.scient. or
Siv.ing., i.e. M.Sc. level) qualifications with a level corresponding
at least "B". This represents approximately five years of full time
studies after completion of European Upper Secondary
School/International Baccalaureate.
For more information see:
http://www.mn.uio.no/english/research/doctoral-degree-and-career/phd-
programme/application/index.html

Average grade calculator, to be taken without Master Thesis
http://www.uio.no/for-ansatte/arbeidsstotte/sta/fs/veiledninger/opptak
/kalkulatorer/kalk.php?type=mn

[ Please feel free to 

[TYPES/announce] Postdoc position in proof theory in Paris

[lutz]

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


  Postdoc position in proof theory in Paris


There is an opening of a postdoc position on structural and
computational proof theory. The position is financed by
the ANR within the project FISP.



The postdoc will be hosted by INRIA and the Laboratoire d'Informatique
(LIX) at the Ecole Polytechnique, one of the "Grand Ecoles" in the French
university system, located in the suburbs of Paris.

The successful candidate will be working within the PARSIFAL team.



Starting date should be in Fall 2017.

Applicants must have a Ph.D. or equivalent in computer science or
mathematics, and should have a strong background in proof theory
and related topics. The principal responsibility of the postdoc
will be to carry out research in the area of proof theory within the
FISP project. There are no teaching duties.

For further information, see


or contact
Lutz Strassburger 

Applications should be sent via email to Lutz Strassburger
 and should include a CV, a research
statement (1-2 pages), and one or two recommendation letters. The
application deadline is

*** April 16, 2017 ***

[TYPES/announce] call for papers: quantifiers and determiners (QUAD, ESSLLI 2017 Workshop)

[Christian RETORE]

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

QUAD: QUantifiers And Determiners
http://www.lirmm.fr/quad
Toulouse, Monday  July 17 --- Friday July 21:  17:00-18:30 
As part of ESSLLI 2017 
Christian Retoré, LIRMM & université de Montpellier, 
Mark Steedman, University of Edinburgh 

Schedule:

deadline for submissions:  17 Mars 2017 
submission website: https://easychair.org/conferences/?conf=quad2017  
notification to authors:  15 April 2017 
final version due: 19 May 2017 
conference: 17-21 July 2017 

Presentation:

The compositional interpretation of determiners relies on quantifiers  — in a 
general acceptation of this later term which includes generalised quantifiers, 
generics, definite descriptions i.e. any operation that applies to one or 
several formulas with a free variable, binds it  and yields a formula or 
possibly a generic term  (the operator is then called a subnector, following 
Curry). There is a long history of quantification in the Ancient and Medieval 
times at the border between logic and philosophy of language, before the proper 
formalisation of quantification by Frege.

A common solution for natural language semantics is the so-called theory of 
generalised quantifiers. Quantifiers like « some, exactly two, at most three, 
the majority of, most of, few, many, … » are all described in terms of 
functions of two predicates viewed as subsets.

Nevertheless, many mathematical and linguistic questions remain open.

On the mathematical side, little is known about generalised , generalised and 
vague quantifiers, in particular about their proof theory. On the other hand, 
even for standard quantifiers, indefinites and definite descriptions, there 
exist alternative formulations with choice functions and generics or subnectors 
(Russell’s iota, Hilbert-Bernays, eta, epsilon, tau). The computational aspects 
of these logical frameworks are also worth studying, both for computational 
linguistic software and for the modelling of the cognitive processes involved 
in understanding or producing sentences involving quantifiers.

On the linguistic side, the relation between the syntactic structure and its 
semantic interpretation, quantifier raising, underspecification, scope issues,… 
 are not fully satisfactory. Furthermore extension of linguistic studies to 
various languages have shown how complex quantification is in natural language 
and its relation to phenomena like generics, plurals,  and mass nouns.

Finally, and this can be seen as a link between formal models of quantification 
and natural language,  there by now exist psycholinguistic experiments that 
connect formal models and their computational properties to the actual way 
human do process sentences with quantifiers, and handle their inherent 
ambiguity, complexity, and difficulty in understanding. 

All those aspects are connected in the didactics of mathematics and computer 
science: there are specific difficulties to teach (and to learn) how to  
understand, manipulate,  produce and  prove quantified statements, and to 
determine  the proper level of formalisation between bare logical formulas and 
written or spoken natural language. 

This workshop aims at gathering  mathematicians, logicians, linguists, computer 
scientists  to present their latest advances in the study of quantification.

Among the topics that wil be addressed are the following :

• new ideas in quantification in mathematical logic, both model theory 
and proof theory:
• choice functions,
• subnectors (Russell’s iota, Hilbert’s epsilon and tau),
• higher order quantification,
• quantification in type theory
• studies of the lexical, syntactic and semantic of quantification in 
various languages
• semantics of noun phrases
• generic noun phrases
• semantics of plurals and mass nouns
• experimental study of quantification and generics
• computational applications of quantification and polarity especially 
for question-answering.
• quantification in the didactics of mathematics and computer science. 


Submissions: 

The program committee is looking for  contributions introducing 
new viewpoints on quantification and determiners,  
the novelty being either in the mathematical logic framework 
or in the linguistic description  or in the cognitive modelling. 
Submitting purely original work is not mandatory,
but authors should clearly mention that the work is not original,
and why they want to present it at this workshop 
(e.g. new viewpoint on already published results) 

Submissions should be 
- 12pt font (at least) 
- 1inch/2.5cm margins all around (at least) 
- less than 2 pages (references exluded)  
- with an abstract of less then 100 words 
and they should be submitted in PDF by easychair here: 
https://easychair.org/conferences/?conf=quad2017

In case the committee 

[TYPES/announce] FSCD 2017 - Second Call for Papers

[Sandra Alves]

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

  *** Apologies for multiple copies, please redistribute ***

   CALL FOR PAPERS

  Second International Conference on
  Formal Structures for Computation and Deduction (FSCD'17)

  4 -- 7 September 2017, Oxford, UK
(in-cooperation with the ACM SIGLOG and SIGPLAN and co-located with ICFP 2017)
 http://www.cs.ox.ac.uk/conferences/fscd2017/

FSCD (http://fscdconference.org/) covers all aspects of formal
structures for computation and deduction from theoretical foundations
to applications.  Building on two communities, RTA (Rewriting
Techniques and Applications) and TLCA (Typed Lambda Calculi and
Applications), FSCD embraces their core topics and broadens their
scope to closely related areas in logics, proof theory and new
emerging models of computation such as quantum computing or homotopy
type theory.

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

Abstract Deadline: 7 April 2017
Submission Deadline:   14 April 2017
Rebuttal:   29--31 May   2017
Notification:  14 June  2017 
Camera-Ready:7 July  2017 

Suggested, but not exclusive, list of topics for submission are:

1. Calculi: Lambda calculus * Concurrent calculi * Logics * Rewriting
   systems * Proof theory * Type theory and logical frameworks

2. Methods in Computation and Deduction: Type systems * Induction and
   coinduction * Matching, unification, completion, and orderings *
   Strategies * Tree automata * Model checking * Proof search and
   theorem proving * Constraint solving and decision procedures

3. Semantics: Operational semantics * Abstract machines * Game
   Semantics * Domain theory and categorical models * Quantitative
   models

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

5. Tools and Applications: Programming and proof environments *
   Verification tools * Libraries for proof assistants and interactive
   theorem provers * Case studies in proof assistants and interactive
   theorem provers * Certification

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

SUBMISSION GUIDELINES Submissions can be made in two categories.
Regular research papers are limited to 15 pages and must present
original research which is unpublished and not submitted
elsewhere. System descriptions are limited to 10 pages and must
describe a working system which has not been published or submitted
elsewhere.  Submissions must be formatted using the LIPIcs style files
and submitted via EasyChair.  Complete instructions on submitting a
paper can be found on the conference web site.

SPECIAL ISSUES Full versions of several accepted papers, to be
selected by the program committee, will be invited for submission to a
special issue of Logical Methods in Computer Science.

BEST PAPER AWARD BY JUNIOR RESEARCHERS The program committee will
consider declaring this award to a paper in which all authors are
junior researchers: a junior researcher is a person who is either a
student or whose PhD award date is less than three years from the
first day of the meeting.

PROGRAM COMMITTEE CHAIR
  Dale Miller, Inria Saclay & LIX 

PROGRAM COMMITTEE
  Andreas Abel, Gothenburg Univ.  
  Elvira Albert, Complutense Madrid 
  Maria Alpuente, TU Valencia 
  Takahito Aoto, Niigata Univ.
  Zena Ariola, Univ. Oregon 
  Federico Aschieri, TU Wien 
  Stefano Berardi, Univ.  Turin 
  Lars Birkedal, Aarhus Univ.
  Filippo Bonchi, CNRS, ENS Lyon 
  Pierre Clairambault, CNRS, ENS Lyon
  Ugo Dal Lago, Univ. Bologna 
  Herman Geuvers, Radboud Univ. 
  Silvia Ghilezan, Univ.  Novi Sad 
  Juergen Giesl, RWTH Aachen 
  Hugo Herbelin, Inria Paris
  Jan Hoffmann, Carnegie Mellon 
  Deepak Kapur, Univ.  New Mexico 
  Paul Blain Levy, Univ.  Birmingham 
  Paulo Oliva, QMUL, London 
  Vincent van Oostrom, Univ. Innsbruck 
  Daniela Petrisan, LIAFA, Paris 
  Femke van Raamsdonk, VU Univ. Amsterdam 
  Grigore Rosu, Univ. Illinois 
  Albert Rubio, UPC-BarcelonaTech
  Paula Severi, Univ.  Leicester 
  Bas Spitters, Aarhus Univ.  
  Aaron Stump, Univ. Iowa 
  Kazushige Terui, Kyoto Univ.
  Rene Thiemann, Univ.  Innsbruck 
  Sophie Tison, Lille Univ.

CONFERENCE CHAIR
  Sam Staton, Univ. of Oxford

WORKSHOP CHAIR
  Jamie Vicary, Univ. of Oxford

PUBLICITY CHAIR
  Sandra Alves, Univ. of Porto

FSCD STEERING COMMITTEE T. Altenkirch (Univ. Nottingham), S. Alves