[Hol-info] CFP - 5th Workshop on Practical Aspects of Automated Reasoning

[Geoff Sutcliffe]

FIRST CALL FOR PAPERS

PAAR-2016 - 5th Workshop on Practical Aspects of Automated Reasoning
July 2nd, 2016.  Coimbra, Portugal

Deadline: May 2nd, 2016
http://cs.ru.nl/paar16/

General Information

  The 5th Workshop on Practical Aspects of Automated Reasoning will
  be held on July 2nd, 2016 in Coimbra, Portugal.  PAAR is associated
  with the 8th International Joint Conference on Automated Reasoning
  (IJCAR-2016).

Scope

  PAAR provides a forum for developers of automated reasoning
  tools to discuss and compare different implementation
  techniques, and for users to discuss and communicate their
  applications and requirements. The workshop will bring
  together different groups to concentrate on practical aspects
  of the implementation and application of automated reasoning
  tools. It will allow researchers to present their work in
  progress, and to discuss new implementation techniques and
  applications.

Topics include but are not limited to:
o automated reasoning in propositional, first-order,
  higher-order and non-classical logics;
o implementation of provers (SAT, SMT, resolution, tableau,
  instantiation-based, rewriting, logical frameworks, etc);
o automated reasoning tools for all kinds of practical
  problems and applications;
o pragmatics of automated reasoning within proof assistants;
o practical experiences, usability aspects, feasibility
  studies;
o evaluation of implementation techniques and automated
  reasoning tools;
o performance aspects, benchmarking approaches;
o non-standard approaches to automated reasoning,
  non-standard forms of automated reasoning, new
  applications;
o implementation techniques, optimisation techniques,
  strategies and heuristics, fairness;
o support tools for prover development;
o system descriptions and demos.
  We are particularly interested in contributions that help the
  community to understand how to build useful reasoning systems
  in practice, and how to apply existing systems to real
  problems.

Paper Submissions

  Researchers interested in participating are invited to submit either
  an extended abstract (up to 8 pages) or a regular paper (up to 15
  pages) via EasyChair at
  https://easychair.org/conferences/?conf=paar2016. Submissions will
  be refereed by the program committee, which will select a balanced
  program of high-quality contributions. Short submissions that could
  stimulate fruitful discussion at the workshop are particularly
  welcome.

  Submissions should be prepared in LaTeX using the EasyChair proceedings
  style. The package containing the class file and its user guide and
  some helper tools can be downloaded from
  http://www.easychair.org/publications/easychair.zip. PAAR proceedings
  will be published electronically in the EasyChair Proceedings in
  Computing (EPiC) series.

  If quality and quantity of the submissions warrants this, we plan to
  produce a special issue of a recognized journal on the topic of the
  workshop.

Important Dates

  Paper submission deadline: May 2nd, 2016 (Anywhere on the planet)
  Notification: May 23rd, 2016
  Camera ready versions due: June 6th, 2016
  Workshop: July 2nd, 2016

Program Committee

  June Andronick, NICTA and University of New South Wales, Australia
  Peter Baumgartner, NICTA/Australian National University, Australia
  Christoph Benzmueller, Freie Universitaet Berlin, Germany
  Armin Bierre, Johannes Kepler University, Austria
  Nikolaj Bjorner, Microsoft Research, USA
  Simon Cruanes, Loria, INRIA, France
  Hans de Nivelle, University of Wroclaw, Poland
  Pascal Fontaine, Loria, INRIA, University of Lorraine, France (co-chair)
  Vijay Ganesh, University of Waterloo, Canada
  Alberto Griggio, FBK-IRST, Italy
  John Harrison, Intel, USA
  Marijn Heule, The University of Texas at Austin, USA
  Dejan Jovanovic, SRI International, USA
  Yevgeny Kazakov, The University of Ulm, Germany
  Chantal Keller, LRI, Universite Paris-Sud, France
  Boris Konev, The University of Liverpool, UK
  Konstantin Korovin, The University of Manchester, UK
  Laura Kovacs, Chalmers University, Sweden
  Jens Otten, University of Potsdam, Germany
  Nicolas Peltier, CNRS - LIG, France
  Ruzica Piskac, Yale University, USA
  Giles Reger, The University of Manchester, UK
  Andrew Reynolds, EPFL, Switzerland
  Philipp Ruemmer, Uppsala University, Sweden
  Uli Sattler, The University of Manchester, UK
  Renate A. Schmidt, The University of Manchester, UK
  Stephan Schulz, DHBW Stuttgart, Germany (co-chair)
  Geoff Sutcliffe, University of Miami, USA
  Josef Urban, Czech Technical University in Prague, Czech Republic (co-chair)
  Uwe Waldmann, MPI Saarbruecken, Germany


--
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.

[Hol-info] FORMATS 2016 - Second Call for Papers

[Sebastian Gerwinn]

[ Apologies for cross posting ]

-

FORMATS 2016

  14th International Conference on
 Formal Modeling and Analysis of Timed Systems

  Second Call for Paper
http://formats2016.lsv.fr

FORMATS'16 takes place at Hotel Chateau Laurier in Québec City,
Canada, where it is colocated with CONCUR'16 and QEST'16.
-



Objectives
--

Control and analysis of the timing of computations is crucial to many
domains of system engineering, be it, e.g., for ensuring timely
response to stimuli originating in an uncooperative environment or for
synchronizing components in VLSI. Reflecting this broad scope, timing
aspects of systems from a variety of domains have been treated
independently by different communities in computer science and
control. Researchers interested in semantics, verification and
performance analysis study models such as timed automata and timed
Petri nets, the digital design community focuses on propagation and
switching delays, while designers of embedded controllers have to take
account of the time taken by controllers to compute their responses
after sampling the environment, as well as of the dynamics of the
controlled process during this span.

Timing-related questions in these separate disciplines do have their
particularities. However, there is a growing awareness that there are
basic problems that are common to all of them. In particular, all
these sub-disciplines treat systems whose behaviour depends upon
combinations of logical and temporal constraints; namely, constraints
on the temporal distances between occurrences of events. Often, these
constraints cannot be separated, as intrinsic dynamics of processes
couples them, necessitating models, methods, and tools facilitating
their combined analysis. Reflecting this fact, FORMATS'16 will
feature a special session on hybrid discrete-continuous systems.


Topics
--

The aim of FORMATS is to promote the study of fundamental and
practical aspects of timed systems, and to bring together researchers
from different disciplines that share interests in modelling and
analysis of timed systems and, as a generalization, hybrid
systems. Typical topics include (but are not limited to):

* Foundations and Semantics:

Theoretical foundations of timed systems and languages; new models
and logics or analysis and comparison of existing models (like
automata, Petri nets, or process algebras involving quantitative
time; hybrid automata; probabilistic automata and logics).

* Methods and Tools:

Techniques, algorithms, data structures, and software tools for
analyzing or synthesizing timed or hybrid systems and for resolving
temporal constraints (scheduling, worst-case execution time analysis,
optimization, model checking, testing, constraint solving, etc.)


* Applications:

Adaptation and specialization of timing technology in application
domains in which timing plays an important role (real-time software,
embedded control, hardware circuits, and problems of scheduling in
manufacturing and telecommunication).


Paper Submission


FORMATS'16 solicits high-quality papers reporting research results
and/or experience reports related to the topics mentioned
above. Submitted papers must contain original, unpublished
contributions, not submitted for publication elsewhere. The papers
should be submitted electronically in PDF, following the Springer LNCS
style guidelines. Submissions should not exceed 15 pages in length,
but may be supplemented with a clearly marked appendix, which will be
reviewed at the discretion of the program committee. Each paper will
undergo a thorough review process.

Papers are to be submitted electronically via the EasyChair online
submission system:

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


The proceedings of FORMATS'16 will be published by Springer in the
Lecture Notes in Computer Science series. A special issue dedicated to
FORMATS will be hosted in a topical journal, collecting the extensions
of papers selected by quality and subject to additional revision.




Important Dates
---

Abstract Submission: April 15, 2016
Paper Submission: April 22, 2016
Notification: June 4, 2016
Final paper due: June 11, 2016
Conference: August 24-26, 2016


General Chair
-

Josée Desharnais, (U. Laval, Canada)


Program Comittee


S. Akshay, (IIT Bombay, India)
Béatrice Bérard, (U. Paris 6, France)
Hanifa Boucheneb, (U. Montréal, Canada)
Laura Carnevali, (U. Firenze, Italy)
Franck Cassez, (U. Macquarie, Australia)
Martin Fränzle, (U. Oldenburg, Germany), (chair)
Gilles Geeraerts, (ULB, Belgium)
Michael R. Hansen, (DTU, Denmark)
Boudewijn Haverkort, (U. Twente, NL)
Franjo Ivancic, (Google, USA)
Oded Maler, (VERIMAG, CNRS-UGA, France)
Nicolas Markey, (U. 

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

[Ramana Kumar]

If you want to build HOL with Poly/ML, you should run
  poly < tools/smart-configure.sml
before running bin/build.

On 2 March 2016 at 13:18, 康漫 <956066...@qq.com> wrote:

> Thank you for your reply!
> My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10
> 14:27:30 2014)], where Moscow ML version 2.01 (January 2004). Then from
> https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and
> pointed ""bin/build". Then I got HOL-4 [Kananaskis 10 (stdknl, built Mon
> Feb 29 21:47:05 2016)],where Moscow ML version 2.01 (January 2004).
> I Opened HOL4, print"open listTheory;", I still can't use LENGTH_TAKE_EQ,
> it responed "Unbound value component: listTheory.LENGTH_TAKE_EQ". I had
> downloaded the files in https://github.com/HOL-Theorem-Prover/HOL. How to
> add it to HOL4's directory? After that ,I could print  "open listTheory;"
> in HOL4, and use LENGTH_TAKE_EQ.
>
> Thanks.
>
>
>
> -- Original --
> *From: * "hol-info-request";;
> *Date: * Wed, Mar 2, 2016 06:31 AM
> *To: * "hol-info";
> *Subject: * hol-info Digest, Vol 118, Issue 1
>
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net
>
> You can reach the person managing the list at
> hol-info-ow...@lists.sourceforge.net
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of hol-info digest..."
>
>
> Today's Topics:
>
>1. Re: How to transform list format from "(cx l q p)" to "l"
>   (Anthony Fox)
>2. Re: Existential quantifier length (Michael Norrish)
>3. ? Summer School on Real-World Crypto and Privacy, June 5-10,
>   Croatia (Veelasha)
>
>
> --
>
> Message: 1
> Date: Mon, 29 Feb 2016 10:25:51 +
> From: Anthony Fox 
> Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
> to "l"
> To: ?? <956066...@qq.com>
> Cc: hol-info 
> Message-ID: <6c0cb742-6c45-45b0-80bd-78737f4cd...@cam.ac.uk>
> Content-Type: text/plain; charset=utf-8
>
> Which version of HOL4 are you using? The definitions of TAKE and DROP were
> altered in Jan 2008 (around about the time of kananaskis-5).
>
> With the latest version of HOL4 Jeremy Dawson?s suggestion works fine for
> me. The proof seems to be trivial. (I?ve not tried it with older versions
> of HOL4.) How exactly did you define ?cx??
>
> With
>
> val cx_def = Define`
>   (cx [] p q = p) /\
>   (cx (h :: t) p q = TAKE h (cx t p q) ++ DROP h (cx t q p))`
>
> we have
>
> val th = Q.prove(
>   `!p q l. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
>   Induct_on `l` THEN RW_TAC list_ss [cx_def, listTheory.LENGTH_TAKE_EQ])
>
> To get something closer to your definition of ?cx? I did
>
> val cx_def = tDefine "cx" `
>   (cx [] p q = p) /\
>   (cx (h :: t) p q =
>TAKE (HD (h :: t)) (cx (TL (h :: t)) p q) ++
>DROP (HD (h :: t)) (cx (TL (h :: t)) q p))`
>   (WF_REL_TAC `measure (\(x,y,z). LENGTH x)` THEN simp [])
>
> but the proof worked without modification.
>
> Regards,
> Anthony
>
> > On 29 Feb 2016, at 07:38, ?? <956066...@qq.com> wrote:
> >
> > Hi,Jeremy
> > Thank you for your reply!
> > I tried. But it can't work.
> > It responsed:
> > - e (RW_TAC list_ss [LENGRH_DROP]);
> > OK..
> > Exception raised at Tactical.VALID:
> > Invalid tactic
> > ! Uncaught exception:
> > ! HOL_ERR
> > I think the reason is that the format of "(cx l q p)"  is not equal to
> "l", though they are the same type "bool list".
> > Thank you!
> >
> > -- Original --
> > From:  "hol-info-request";;
> > Date:  Mon, Feb 29, 2016 01:08 PM
> > To:  "hol-info";
> > Subject:  hol-info Digest, Vol 117, Issue 9
> >
> > Send hol-info mailing list submissions to
> > hol-info@lists.sourceforge.net
> >
> > To subscribe or unsubscribe via the World Wide Web, visit
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> > or, via email, send a message with subject or body 'help' to
> > hol-info-requ...@lists.sourceforge.net
> >
> > You can reach the person managing the list at
> > hol-info-ow...@lists.sourceforge.net
> >
> > When replying, please edit your Subject line so it is more specific
> > than "Re: Contents of hol-info digest..."
> >
> >
> > Today's Topics:
> >
> >1. How to transform list format from "(cx l q p)" to "l" ( Ada )
> >2. Re: How to transform list format from "(cx l q p)" to "l"
> >   (Jeremy Dawson)
> >3. Two postdoc positions - Reasoning about concurrency and
> >   distribution - Imperial College London (Petar Maksimovic)
> >
> >
> > 

[Hol-info] 2nd CFP ICLP 2016, New York City: 32nd International Conference on Logic Programming, Oct 17-21

[Peter Schueller]

Second Call For Papers
  32nd International Conference on Logic Programming

  New York City, USA
 October 17-21, 2016

   http://software.imdea.org/Conferences/ICLP2016/

Conference Scope

Since  the first conference held in Marseilles in 1982, ICLP has been the pre-
mier international conference for presenting research  in  logic  programming.
Contributions  are sought in all areas of logic programming, including but not
restricted to:


 - Theory: Semantic Foundations, Formalisms, Nonmonotonic Reasoning, Knowledge
   Representation.

 - Implementation: Compilation, Virtual Machines, Parallelism, Constraint Han-
   dling Rules, Tabling.

 - Environments: Program Analysis, Transformation,  Validation,  Verification,
   Debugging, Profiling, Testing.

 - Language  Issues:  Concurrency,  Objects,  Coordination,  Mobility,  Higher
   Order, Types, Modes, Assertions, Programming Techniques.

 - Related Paradigms: Inductive and Co-inductive Logic Programming, Constraint
   Logic Programming, Answer-Set Programming, SAT-Checking.

 - Applications:  Databases,  Big Data, Data Integration and Federation, Soft-
   ware Engineering,  Natural  Language  Processing,  Web  and  Semantic  Web,
   Agents, Artificial Intelligence, Bioinformatics, and Education.


In  addition  to  the  presentations of accepted papers, the technical program
will include invited talks, advanced tutorials, the doctoral  consortium,  and
several workshops.

Important Dates

Paper registration (abstract):  22 April, 2016
Submission deadline:29 April, 2016
Notification to authors:17 June, 2016
Revision deadline (when needed):8 July, 2016
Final notification: 22 July, 2016
Camera-ready copy due:  5 Aug, 2016
Conference: 17-21 Oct, 2016

Submission Details

Submissions  of  regular papers must be made in the condensed TPLP format (see
http://software.imdea.org/Conferences/ICLP2016/TPLP-ICLP-2016.tar)  via  Easy-
Chair  (see  http://www.easychair.org/conferences/?conf=iclp2016).   A regular
paper must not exceed 14 pages including the bibliography, but the  paper  may
be  supplemented  with  appendices for proofs and details of datasets which do
not count towards this limit and which will be available as appendices to  the
published paper. We accept three kinds of papers:


 - Technical  papers  for technically sound, innovative ideas that can advance
   the state of logic programming;

 - Application papers that impact interesting application domains;

 - System and tool papers which emphasize  novelty,  practicality,  usability,
   and availability of the systems and tools described.


Application, system, and tool papers need to be clearly marked in their title.
All submissions must be written in English and describe  original,  previously
unpublished research, and must not simultaneously be submitted for publication
elsewhere.  Papers of the highest quality will be selected to be published  in
the journal of Theory and Practice of Logic Programming (TPLP), Cambridge Uni-
versity Press (CUP). In order to ensure the  quality  of  the  final  version,
papers  may  be subject to more than one round of refereeing (within the deci-
sion period).

The program committee may recommend some papers to be published  as  technical
communications.  Technical  communications (TCs) will be published by Dagstuhl
Publishing   in   theOpenAccessSeriesinInformatics(OASIcs)
(http://www.dagstuhl.de/publikationen/oasics/).   These  TC  papers should not
exceed 14 pages including bibliography.  Authors can  also  elect  to  convert
their  submissions  into extended abstracts, of 2 or 3 pages, for inclusion in
the TCs.  This should allow authors to submit a long version  elsewhere.   All
regular papers and regular TCs will be presented during the conference.

Doctoral  consortium position papers, of between 10 and 14 pages, will also be
published as TCs.

Authors of accepted papers will, by default, be automatically included in  the
list  of  ALP  members, who will receive quarterly updates from the Logic Pro-
gramming Newsletter at no cost.


Conference Organization

General Chairs:

Michael Kifer   Stony Brook University, USA
Neng-Fa ZhouCity University of New York, USA

Program Chairs:

Manuel  Carro   UPM and IMDEA Software Institute, Spain
AndyKingUniversity of Kent, UK

Workshop Chair:

MarcelloBalduccini  Drexel University, USA

Publicity Chair:

Peter   Schueller   Marmara University, Turkey

Doctoral Consortium Chairs:

Marina  De Vos  University of Bath, UK
NedaSaeedloei   University of Minnesota Duluth, USA

Programming Contest Chair:

PaulFodor   Stony Brook 

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

[Michael Norrish]

It is true that LENGTH_TAKE_EQ is not in Kananaskis-10 (it appeared in the 
repository on 14 August 2015).

You could add it to your development manually: its conclusion is

   LENGTH (TAKE n xs) = if n <= LENGTH xs then n else LENGTH xs

Michael

On 2 Mar 2016, at 13:18, 康漫 <956066...@qq.com> wrote:

Thank you for your reply!
My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10 14:27:30 
2014)], where Moscow ML version 2.01 (January 2004). Then from 
https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and pointed 
""bin/build". Then I got HOL-4 [Kananaskis 10 (stdknl, built Mon Feb 29 
21:47:05 2016)],where Moscow ML version 2.01 (January 2004).
I Opened HOL4, print"open listTheory;", I still can't use LENGTH_TAKE_EQ, it 
responed "Unbound value component: listTheory.LENGTH_TAKE_EQ". I had downloaded 
the files in https://github.com/HOL-Theorem-Prover/HOL. How to add it to HOL4's 
directory? After that ,I could print  "open listTheory;" in HOL4, and use 
LENGTH_TAKE_EQ.

Thanks.



-- Original --
From:  
"hol-info-request";>;
Date:  Wed, Mar 2, 2016 06:31 AM
To:  
"hol-info">;
Subject:  hol-info Digest, Vol 118, Issue 1

Send hol-info mailing list submissions to
hol-info@lists.sourceforge.net

To subscribe or unsubscribe via the World Wide Web, visit
https://lists.sourceforge.net/lists/listinfo/hol-info
or, via email, send a message with subject or body 'help' to
hol-info-requ...@lists.sourceforge.net

You can reach the person managing the list at
hol-info-ow...@lists.sourceforge.net

When replying, please edit your Subject line so it is more specific
than "Re: Contents of hol-info digest..."


Today's Topics:

   1. Re: How to transform list format from "(cx l q p)" to "l"
  (Anthony Fox)
   2. Re: Existential quantifier length (Michael Norrish)
   3. ? Summer School on Real-World Crypto and Privacy, June 5-10,
  Croatia (Veelasha)


--

Message: 1
Date: Mon, 29 Feb 2016 10:25:51 +
From: Anthony Fox >
Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
to "l"
To: ?? <956066...@qq.com>
Cc: hol-info 
>
Message-ID: 
<6c0cb742-6c45-45b0-80bd-78737f4cd...@cam.ac.uk>
Content-Type: text/plain; charset=utf-8

Which version of HOL4 are you using? The definitions of TAKE and DROP were 
altered in Jan 2008 (around about the time of kananaskis-5).

With the latest version of HOL4 Jeremy Dawson?s suggestion works fine for me. 
The proof seems to be trivial. (I?ve not tried it with older versions of HOL4.) 
How exactly did you define ?cx??

With

val cx_def = Define`
  (cx [] p q = p) /\
  (cx (h :: t) p q = TAKE h (cx t p q) ++ DROP h (cx t q p))`

we have

val th = Q.prove(
  `!p q l. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
  Induct_on `l` THEN RW_TAC list_ss [cx_def, listTheory.LENGTH_TAKE_EQ])

To get something closer to your definition of ?cx? I did

val cx_def = tDefine "cx" `
  (cx [] p q = p) /\
  (cx (h :: t) p q =
   TAKE (HD (h :: t)) (cx (TL (h :: t)) p q) ++
   DROP (HD (h :: t)) (cx (TL (h :: t)) q p))`
  (WF_REL_TAC `measure (\(x,y,z). LENGTH x)` THEN simp [])

but the proof worked without modification.

Regards,
Anthony

> On 29 Feb 2016, at 07:38, ?? <956066...@qq.com> 
> wrote:
>
> Hi,Jeremy
> Thank you for your reply!
> I tried. But it can't work.
> It responsed:
> - e (RW_TAC list_ss [LENGRH_DROP]);
> OK..
> Exception raised at Tactical.VALID:
> Invalid tactic
> ! Uncaught exception:
> ! HOL_ERR
> I think the reason is that the format of "(cx l q p)"  is not equal to "l", 
> though they are the same type "bool list".
> Thank you!
>
> -- Original --
> From:  
> "hol-info-request";>;
> Date:  Mon, Feb 29, 2016 01:08 PM
> To:  
> "hol-info">;
> Subject:  hol-info Digest, Vol 117, Issue 9
>
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net
>
> You can reach the person managing the list at
>