[Hol-info] 13th International Workshop on the Implementation of Logics

[geoff]

 The 13th International Workshop on the Implementation of Logics
   http://www.eprover.org/EVENTS/IWIL-2018.html

 CALL FOR PAPERS
Deadline: October 1, 2018.


The 13th International Workshop on the Implementation of Logics will be held on
16th November 2018, in conjunction with the 22nd International Conference on 
Logic for Programming, Artificial Intelligence, and Reasoning, at the Haile
Resort in Awassa, Ethiopia.

We are looking for contributions describing implementation techniques for and
implementations of automated reasoning programs, theorem provers for various
logics, logic programming systems, and related technologies. Topics of interest
include, but are not limited to:

+ Propositional logic and decision procedures, including SMT
+ First-order and higher order logics
+ Non-classical logics, including modal, temporal, description, non-monotonic
  reasoning
+ Formal foundations for efficient implementation of logics
+ Data structures and algorithms for the efficient representation and
  processing of logical concepts
+ Proof/model search organization and heuristics for logical reasoning systems
+ Data analysis and machine learning approaches to search control
+ Techniques for proof/model search visualization and analysis
+ Reasoning with ontologies and other large theories
+ Implementation of efficient theorem provers and model finders for different
  logics
+ System descriptions of logical reasoning systems
+ Issues of reliability, witness generation, and  witness verification
+ Evaluation and benchmarking of provers and other logic-based systems
+ I/O standards and communication between reasoning systems

We are particularly interested in contributions that help the community to
understand how to build useful and powerful reasoning systems, and how to apply
them in practice.

Researchers interested in participating are invited to submit a position
statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15
pages) via the EasyChair page for IWIL-2018.
 https://easychair.org/conferences/?conf=iwil2018

Submissions will be refereed by the program committee, which will select a
balanced program of high-quality contributions.

Submissions should be in standard-conforming PDF. Final versions will be
required to be submitted in LaTeX using the easychair.cls class file. The
proceedings will be published as a volume of Kalpa Publications in
Computing.

Important Dates:

+ Submission of papers/abstracts:  October 1st, 2018
+ Notification of acceptance:  October 12th, 2018
+ Camera ready versions due:   October 29th, 2018
+ Workshop:November 16th, 2018

Program committee (so far - more coming):

Konstantin Korovin (Co-Chair)  University of Manchester
Stephan Schulz (Co-Chair)  DHBW Stuttgart
Martin Suda (Co-Chair) Czech Technical University in Prague
Geoff SutcliffeUniversity of Miami


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Ramana Kumar]

I think this is false. Here's a proof of the opposite, with the type of f
instantiated to a num set generator:

val thm = Q.prove(
`¬(
  ∀(f:num->num->bool) a sp.
  (f 0 = ∅) ∧
  (∀n. f n ⊆ f (SUC n)) ∧
  (∀n. f n ⊆ sp) ∧
  (BIGUNION (IMAGE f 핌(:num)) = sp) ∧
  (a ⊆ sp) ⇒
 ∃x. a ⊆ f x)`,
  rw[]
  \\ qexists_tac`count`
  \\ qexists_tac`UNIV`
  \\ rw[SUBSET_DEF, PULL_EXISTS]
  >- metis_tac[]
  >- (
rw[Once EXTENSION]
\\ qexists_tac`count (SUC x)`
\\ rw[] )
  >- (
rw[EXTENSION]
\\ qexists_tac`SUC x`
\\ rw[] ));


On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe) 
wrote:

> sorry, I also have this necessary assumption:
>
>  5.  BIGUNION (IMAGE f 핌(:num)) = sp
>
> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> > Hi,
> >
> > I ran into the following goal in the proof of a big theorem:
> >
> >   ∃x. a ⊆ f x
> >   
> > 3.  f 0 = ∅
> > 4.  ∀n. f n ⊆ f (SUC n)
> >20.  ∀n. f n ⊆ sp
> >21.  a ⊆ sp
> >
> > I have an increasing sequence of sets (f n) from empty to the whole
> space (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I
> can always choose a big enough index x such that (f x) will contain “a”.
> But how can I make this argument formal?
> >
> > thanks,
> >
> > Chun
> >
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] NFM 2019 First Call For Papers- 11th Annual NASA Formal Methods Symposium

[Kristin Yvonne Rozier]

 The Eleventh NASA Formal Methods Symposium

 https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html

   7 - 9 May 2019
    Rice University, Houston, Texas, USA



Theme of the Symposium:
---
The widespread use and increasing complexity of mission-critical and 
safety-critical systems at NASA and in the aerospace industry require 
advanced techniques that address these systems' specification, design, 
verification, validation, and certification requirements. The NASA 
Formal Methods Symposium (NFM) is a forum to foster collaboration 
between theoreticians and practitioners from NASA, academia, and 
industry. NFM's goals are to identify challenges and to provide 
solutions for achieving assurance for such critical systems.


New developments and emerging applications like autonomous software for 
uncrewed deep space human habitats, caretaker robotics, Unmanned Aerial 
Systems (UAS), UAS Traffic Management (UTM), and the need for 
system-wide fault detection, diagnosis, and prognostics provide new 
challenges for system specification, development, and verification 
approaches. The focus of these symposiums are on formal techniques and 
other approaches for software assurance, including their theory, current 
capabilities and limitations, as well as their potential application to 
aerospace, robotics, and other NASA-relevant safety-critical systems 
during all stages of the software life-cycle.


The NASA Formal Methods Symposium is an annual event organized by the 
NASA Formal Methods (NFM) Steering Committee, comprised of researchers 
spanning several NASA centers. NFM 2019 
(https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html) is being 
co-organized by Rice University and NASA- Johnson Space Center in 
Houston, TX.


Topics of Interest:
---
We encourage submissions on cross-cutting approaches that bring together 
formal methods and techniques from other domains such as probabilistic 
reasoning, machine learning, control theory, robotics, and quantum 
computing among others.
    * Formal verification, including theorem proving, model checking, 
and static analysis

    * Advances in automated theorem proving including SAT and SMT solving
    * Use of formal methods in software and system testing
    * Run-time verification
    * Techniques and algorithms for scaling formal methods, such as 
abstraction and symbolic methods, compositional techniques, as well as 
parallel and/or distributed techniques

    * Code generation from formally verified models
    * Safety cases and system safety
    * Formal approaches to fault tolerance
    * Theoretical advances and empirical evaluations of formal methods 
techniques for safety-critical systems, including hybrid and embedded 
systems

    * Formal methods in systems engineering and model-based development
    * Correct-by-design controller synthesis
    * Formal assurance methods to handle adaptive systems


Important Dates:

Abstract Submission:  7 Dec 2018
Paper Submission:    14 Dec 2018
Paper Notifications: 22 Feb 2019
Camera-ready Papers: 22 Mar 2019
Symposium:  7-9 May 2019


Location & Cost:

The symposium will take place in the McMurtry Auditorium, Rice 
University, Houston, Texas, USA, May 7--9, 2019.


There will be no registration fee for participants. All interested 
individuals, including non-US citizens, are welcome to attend, to listen 
to the talks, and to participate in discussions; however, all attendees 
must register.



Submission Details:
---
There are two categories of submissions:

   1. Regular papers describing fully developed work and complete 
results (15 pages + references)

   2. Two categories of short papers: (6 pages + references)
   (a) Tool Papers describing novel, publicly-available tools
   (b) Case Studies detailing complete applications of formal methods 
to real systems with publicly-available artifacts


All papers should be in English and describe original work that has not 
been published or submitted elsewhere. All submissions will be fully 
reviewed by members of the Programme Committee. Papers will appear in a 
volume of Springer's Lecture Notes on Computer Science (LNCS), and must 
use LNCS style formatting. Papers should be submitted in PDF format 
here: https://easychair.org/conferences/?conf=nfm2019.



Keynote Speakers:
-
* Virginie Wiels, ONERA, France
* Richard Murray, CalTech, USA
* NASA Panel: Challenges for Future Exploration


Organizers:
---
Moshe Y. Vardi (General Chair)
Julia Badger (PC Chair)
Kristin Yvonne Rozier (PC Chair)


Programme Committee:

Erika Ábrahám, RWTH Aachen University, Germany
Armin Biere, Johannes Kepler University Linz, Austria
Nikolaj Bjorner, Microsoft, USA
Sylvie Boldo, INRIA, France
Jonathan Bowen, London South Bank 

[Hol-info] LPNMR 2019 Call for Papers ** INVITED SPEAKERS TO BE ANNOUNCED

[ggelfond]

 Call for Papers
---

   15th International Conference on
Logic Programming and Non-monotonic Reasoning
   LPNMR 2019

 https://sites.sju.edu/plw/lpnmr-2019/

Philadelphia, USA
  June 4-7, 2019

 Co-located with Datalog 2.0 Workshop
---

AIMS AND SCOPE

 LPNMR 2019 is the fifteenth in the series of international meetings
 on logic programming and non-monotonic reasoning. LPNMR is a forum
 for exchanging ideas on declarative logic programming, non-monotonic
 reasoning, and knowledge representation. The aim of the conference is
 to facilitate interactions between researchers and practitioners
 interested in the design and implementation of logic-based programming
 languages and database systems, and those working in knowledge
 representation and nonmonotonic reasoning. LPNMR strives to encompass
 theoretical and experimental studies that have led or will lead to
 advances in declarative programming and knowledge representation, as
 well as their use in practical applications. A Doctoral Consortium
 will also be a part of the program.

 This year's edition of the conference seeks to raise submissions devoted
 towards use of LPNMR techniques in emerging applications stemming from such
 areas as deep learning, robotics, cybersecurity, modeling cyberphysical
 systems, and human-aware AI. Aspects that have been studied in commonsense
 reasoning, inconsistency tolerance, and handling of dynamic knowledge appear
 essential in enabling these emerging applications to�provide
 explanations and justifications of their outcomes.  LPNMR 2019 aims to
 bring together researchers from LPNMR core areas and application areas of
 the aforementioned kind in order to share research experiences, promote
 collaboration and identify directions for joint future research.


INVITED SPEAKERS

  To be announced


TOPICS

 Authors are invited to submit papers presenting original and unpublished
 research on all aspects of non-monotonic approaches in logic programming
 and knowledge representation. We invite submissions of both long and
 short papers on topics detailed below.

 Conference topics include, but are not limited to:

 1. Foundations of LPNMR Systems:
   * Semantics of new and existing languages;
   * Action languages, causality;
   * Formalization of Commonsense Reasoning and understanding
 its laws and nature;
   * Relationships among formalisms;
   * Complexity and expressive power;
   * Inference algorithms and heuristics for LPNMR systems;
   * Extensions of traditional LPNMR languages such as new logical
 connectives or new inference capabilities;
   * Updates, revision, and other operations on LPNMR systems;
   * Uncertainty in LPNMR systems.

 2. Implementation of LPNMR systems:
   * System descriptions, comparisons, evaluations;
   * Algorithms and novel techniques for efficient evaluation;
   * LPNMR benchmarks.

 3. Applications of LPNMR:
   * Use of LPNMR in Commonsense Reasoning and other areas of KR;
   * LPNMR languages and algorithms in planning, diagnosis, argumentation,
 reasoning with preferences, decision making and policies;
   * Applications of LPNMR languages in data integration and exchange
 systems, software engineering and model checking;
   * Applications of LPNMR to bioinformatics, linguistics, psychology,
 and other sciences;
   * Integration of LPNMR systems with other computational paradigms;
   * Embedded LPNMR: Systems using LPNMR subsystems.


SUBMISSION

 LPNMR 2019 welcomes submissions of long papers (13 pages) or short papers
 (6 pages) in the following categories:

   * Technical papers
   * System descriptions
   * Application descriptions

 The indicated number of pages includes title page, references and
 figures. All submissions will be peer-reviewed and accepted papers will
 appear in the conference proceedings published in the Springer's
 Lecture Notes in Artificial Intelligence (LNAI/LNCS) series. At least one
 author of each accepted paper is expected to register for the conference
 to present the work. Submissions must be written in English, present
 original research, and be formatted according to Springer's guidelines
 and technical instructions available at:


https://www.springer.com/gp/authors-editors/conference-proceedings/conference-proceedings-guidelines

 Paper submission is enabled via the LPNMR 2019 Easychair site:
https://easychair.org/conferences/?conf=lpnmr2019

 Two best papers of general AI interest will be invited for rapid
 publication in the Artificial Intelligence Journal.

 Also, the journal Theory and Practice of Logic Programming will devote
 a special issue for a joint event of LPNMR/Datalog 2.0. Four 

[Hol-info] PhD positions in Programming Language Technology for Security and Privacy

[David Sands]

Chalmers University of Technology in Gothenburg, Sweden invite applications for 
PhD positions in Programming Language Technology for Security and Privacy.

We are looking for applicants with a technical background in the programming 
languages and systems research area, and who have a keen interest in applying 
and developing this technology to create new methods and tools for security and 
privacy of software and systems. You will have a good knowledge in several of 
the following areas: compiler technology, static analysis, type systems, 
programming language semantics, advanced functional programming, program 
verification.

Application deadline: October 10th, 2018. We encourage all applicants who might 
need a visa to visit Sweden to apply as soon as possible.

For details about the employment conditions and how to apply see:

http://www.chalmers.se/en/about-chalmers/Working-at-Chalmers/Vacancies/Pages/default.aspx?rmpage=job=6602=UK

___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Final Call for Papers PADL-19

[Moa Johansson]

21th International Symposium on Practical Aspects of Declarative Languages 
(PADL 2019)

 https://popl19.sigplan.org/track/PADL-2019

Lisbon, Portugal. 14 -15 January 2019.

Co-located with ACM POPL 2019 (https://popl19.sigplan.org/home)

Declarative languages build on sound theoretical bases to provide attractive 
frameworks for application development. These languages have been successfully 
applied to many different real-world situations, ranging from data base 
management to active networks to software engineering to decision support 
systems.

New developments in theory and implementation have opened up new application 
areas. At the same time, applications of declarative languages to novel 
problems raise numerous interesting research issues. Well-known questions 
include designing for scalability, language extensions for application 
deployment, and programming environments. Thus, applications drive the progress 
in the theory and implementation of declarative systems, and benefit from this 
progress as well.

PADL is a well-established forum for researchers and practitioners to present 
original work emphasising novel applications and implementation techniques for 
all forms of declarative concepts, including, functional, logic, constraints, 
etc. Topics of interest include, but are not limited to:

  *   Innovative applications of declarative languages
  *   Declarative domain-specific languages and applications
  *   Practical applications of theoretical results
  *   New language developments and their impact on applications
  *   Declarative languages and software engineering
  *   Evaluation of implementation techniques on practical applications
  *   Practical experiences and industrial applications
  *   Novel uses of declarative languages in the classroom
  *   Practical extensions such as constraint-based, probabilistic, and 
reactive languages.

PADL 2019 welcomes new ideas and approaches pertaining to applications and 
implementation of declarative languages, and is not limited to the scope of the 
past PADL symposia. It will be co-located with the Symposium on Principles of 
Programming Languages (POPL 2019), in Lisbon, Portugal.

Important Dates and Submission Guidelines

Abstracts due:  21 September

Papers due:  28 September

Notification to authors:  26 October

Authors should submit an electronic copy of the full paper in PDF using the 
Springer LNCS format. The submission will be done through EasyChair conference 
system: https://easychair.org/conferences/?conf=padl2019

All submissions must be original work written in English. Submissions must be 
unpublished and not submitted for publication elsewhere. Work that already 
appeared in unpublished or informally published workshops proceedings may be 
submitted but the authors should notify the program chair about the place on 
which it has previously appeared.

PADL 2019 will accept both technical and application papers:

  *   Technical papers must describe original, previously unpublished research 
results. Technical papers must not exceed 15 pages (plus one page of 
references) in Springer LNCS format.
  *   Application papers are a mechanism to present important practical 
applications of declarative languages that occur in industry or in areas of 
research other than Computer Science. Application papers are expected to 
describe complex and/or real-world applications that rely on an innovative use 
of declarative languages. Application descriptions, engineering solutions and 
real-world experiences (both positive and negative) are solicited. The limit 
for application papers is 8 pages in Springer LNCS format but such papers can 
also point to sites with supplemental information about the application or the 
system that they describe.

The proceedings of PADL 2019 will appear in the LNCS series of Springer Verlag: 
https://www.springer.com/gp/computer-science/lncs

Journal Publication for Best Papers

The best papers (as selected by the PC chairs) will be invited to submit a 
longer version for journal publication after the symposium. For papers related 
to logic programming, in the journal Theory and Practice of Logic Programming 
(TPLP),
 and for papers related to functional programming, in Journal of Functional 
Programming 
(JFP).

The authors of these papers will be invited to submit a journal version 
containing at least 30% new material. This will be reviewed by the PC and/or 
the respective journal editors for a swifter reviewing process of the journal 
version.

Such extensions could be explanations for which there was no space, 
illuminating examples and proofs, additional definitions and theorems, further 
experimental results, implementational details and feedback from 
practical/engineering use, extended discussion of related work and such like.

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

sorry, I also have this necessary assumption:

 5.  BIGUNION (IMAGE f 핌(:num)) = sp

> Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi,
> 
> I ran into the following goal in the proof of a big theorem:
> 
>   ∃x. a ⊆ f x
>   
> 3.  f 0 = ∅
> 4.  ∀n. f n ⊆ f (SUC n)
>20.  ∀n. f n ⊆ sp
>21.  a ⊆ sp
> 
> I have an increasing sequence of sets (f n) from empty to the whole space 
> (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I can 
> always choose a big enough index x such that (f x) will contain “a”. But how 
> can I make this argument formal?
> 
> thanks,
> 
> Chun
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

Hi,

I ran into the following goal in the proof of a big theorem:

   ∃x. a ⊆ f x
   
 3.  f 0 = ∅
 4.  ∀n. f n ⊆ f (SUC n)
20.  ∀n. f n ⊆ sp
21.  a ⊆ sp

I have an increasing sequence of sets (f n) from empty to the whole space (sp), 
and I have a single set “a” (⊆ sp). It looks *obvious* that, I can always 
choose a big enough index x such that (f x) will contain “a”. But how can I 
make this argument formal?

thanks,

Chun



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] CPP 2019: Final Call for Papers

[Magnus Myreen]

Certified Programs and Proofs (CPP) is an international forum on
theoretical and practical topics in all areas, including computer
science, mathematics, and education, that consider certification as an
essential paradigm for their work. Certification here means formal,
mechanized verification of some sort, preferably with production of
independently checkable certificates.

In 2019, CPP will be co-located with Principles of Programming
Languages (POPL) in Cascais/Lisbon, Portugal.

Important Dates (AoE, UTC-12h)

 Abstract Deadline: 11 October 2018
 Paper Submission Deadline: 18 October 2018
 Author Notification: 22 November 2018
 Camera-ready deadline: 27 November 2018
 Conference dates: 14 January - 15 January 2019

Topics of interest

We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a suggested
list of topics of interests to CPP. This is a non-exhaustive list and
should be read as a guideline rather than a requirement.

  - certified or certifying programming, compilation, linking, OS
kernels, runtime systems, and security monitors;
  - program logics, type systems, and semantics for certified code;
  - certified decision procedures, mathematical libraries, and
mathematical theorems;
  - proof assistants and proof theory;
  - new languages and tools for certified programming;
  - program analysis, program verification, and proof-carrying code;
  - certified secure protocols and transactions;
  - certificates for decision procedures, including linear algebra,
polynomial systems, SAT, SMT, and unification in algebras of
interest;
  - certificates for semi-decision procedures, including equality,
first-order logic, and higher-order unification;
  - certificates for program termination;
  - logics for certifying concurrent and distributed programs;
  - higher-order logics, logical systems, separation logics, and
logics for security;
  - teaching mathematics and computer science with proof assistants.

Submission Guidelines

Papers should be submitted in PDF format through the EasyChair
submission page at

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

Submitted papers must be formatted following the ACM SIGPLAN
Proceedings format using the acmart format with the sigplan option,
using 10 point font for the main text, and a header for single blind
review submission, e.g.,

\documentclass[sigplan,10pt,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}

Submitted papers should not exceed 12 pages, including tables and
figures, but excluding bibliography. Shorter papers are welcome and
will be given equal consideration.

Submissions must be written in English and provide sufficient detail
to allow the program committee to assess the merits of the paper. They
should begin with a succinct statement of the issues, a summary of the
main results, and a brief explanation of their significance and
relevance to the conference, all phrased for the
non-specialist. Technical and formal developments directed to the
specialist should follow. References and comparisons with related work
should be included. Submitted papers are not allowed to have an
appendix. Papers not conforming to the above requirements concerning
format and length may be rejected without further consideration.

Whenever appropriate, the submission should come along with a formal
development, using whatever prover, e.g., Agda, Coq, Dafny, Elf, HOL,
HOL-Light, Isabelle, Lean, Matita, Mizar, NQTHM, PVS, Vampire,
etc. Such formal developments must be submitted together with the
paper as auxiliary material, and will be taken into account during the
reviewing process. Please do so by including a link to your files in
the text of your paper, or by sending a zip or tar file to the PC
chairs at cpp2...@easychair.org with your paper number included in the
subject of your email.

The results must be unpublished and not submitted for publication
elsewhere, including the proceedings of other published conferences or
workshops. The PC chairs should be informed of closely related work
submitted to a conference or journal in advance of
submission. Original formal proofs of known results in mathematics or
computer science are welcome. One author of each accepted paper is
expected to present it at the conference.


For any questions about the formatting or submission of papers, please
consult the PC chairs (cpp2...@easychair.org).

Conference webpage: https://popl19.sigplan.org/track/CPP-2019


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info