Piotr Trojanek | 23 Oct 13:00 2014

HOL Light-style parsing in HOL4

Dear all,

is it possible to use HOL4 parser in a similar way to `parse_preterm`
from HOL Light?

In HOL Light one can easily build a parser for HOL terms embedded in a
custom language (see hol_light/Examples/prog.ml). In HOL4 it seems
only possible to modify the term grammar (e.g. with add_rule), which
is much less flexible.


Piotr Trojanek

Ramana Kumar | 23 Oct 19:58 2014

omitting a constant from pretty-printing

Hi all,

I would like to add a pretty-printing rule to completely omit a constructor and only print its argument. (I understand this means the resulting output won't parse back to the same input without type inference help.) Is it possible to do this in any way short of making a userprinter?

To be concrete, I have the following:

Datatype`mlstring = strlit (char list)`

and I would like the printer to print


rather than

strlit "hello"

in my HOL-munged LaTeX output. (Userprinters are very difficult to use with the munger, so I would like to avoid them if possible.)

hol-info mailing list
hol-info <at> lists.sourceforge.net
S B Cooper | 22 Oct 22:42 2014

CiE 2015: Evolving Computability, Bucharest, June 29 - July 3, 2015

      COMPUTABILITY IN EUROPE 2015: Evolving Computability
                   Bucharest, Romania
                    June 29 - July 3


Submission Deadline for LNCS:                 11 January 2015
Notification of authors:                         9 March 2015
Deadline for final revisions:                    6 April 2015

CiE 2015 is the 11th conference organized by CiE (Computability
in Europe), a European association of mathematicians, logicians,
computer scientists, philosophers, physicists and others
interested in new developments in computability and their
underlying significance for the real world. Previous meetings
have taken place in Amsterdam (2005), Swansea (2006), Siena
(2007), Athens (2008), Heidelberg (2009), Ponta Delgada (2010),
Sofia (2011), Cambridge (2012), Milan (2013) and Budapest (2014).

Evolution of the universe, and us within it, invite a parallel
evolution in understanding. The CiE agenda - fundamental and
engaged - targets the extracting and developing of computational
models basic to current challenges.  From the origins of life, to
the understanding of human mentality, to the characterising of
quantum randomness - computability theoretic questions arise in
many guises.  The CiE community, this coming year meeting for the
first time in Bucharest, carries forward the search for
coherence, depth and new thinking across this rich and vital
field of research.

In all cases we are looking for fundamental and theoretical
submissions. In line with other conferences in this series, CiE
2015 has a broad scope and provides a forum for the discussion of
theoretical and practical issues in Computability with an
emphasis on new paradigms of computation and the development of
their mathematical theory.

We particularly invite papers that build bridges between
different parts of the research community.

For topics covered by the conference, please visit


  * John Reif (Duke Unversity)
  * Steve Simpson (Pennsylvania State University)


  * Ann Copestake (University of Cambridge)
  * Mircea Dumitru (University of Bucharest, Public Lecture)
  * Pawel Gawrychowski (Max-Planck-Institut fuer Informatik)
  * Julia Knight (University of Notre Dame)
  * Anca Muscholl (Universite Bordeaux)
  * Gheorghe Paun (Romanian Academy)
  * Alexander Razborov (University of Chicago
       and Steklov Mathematical Institute)
  * Vlatko Vedral (University of Oxford)


  * Representing streams
     (Organizers: Joerg Endrullis and Dimtri Hendriks)
  * Automata, logic and infinite games
     (Organizers: Dietmar Berwanger and Ioana Leustean)
  * Reverse mathematics
     (Organizers: Damir Dzhafarov and Alberto Marcone)
  * Classical computability theory
     (Organizers: Marat Arslanov and Steffen Lempp)
  * Bio-inspired computation
     (Organizers: Andrei Paun and Petr Sosik)
  * History and philosophy of computing
     (Organizers: Christine Proust and Marco Benini)


  * Marat Arslanov (Kazan)           * Jeremy Avigad (Pittsburgh)
  * Veronica Becher (Buenos Aires)   * Arnold Beckmann (Swansea)
  * Laurent Bienvenu (Paris)         * Alessandra Carbone (Paris)
  * Gabriel Ciobanu (Iasi)           * S Barry Cooper (Leeds)
  * Laura Crosilla (Leeds)           * Liesbeth De Mol (Ghent)
  * Walter Dean (Warwick)            * Volker Diekert (Stuttgart)
  * Damir Dzhafarov (Storrs, Connecticut)
  * Peter van Emde Boas (Amsterdam)  * Rachel Epstein (Harvard)
  * Johanna Franklin (Hempstead, NY) * Neil Ghani (Glasgow)
  * Joel David Hamkins (New York)    * Rosalie Iemhoff (Utrecht)
  * Emmanuel Jeandel (LORIA)         * Natasha Jonoska (Tampa, FL)
  * Antonina Kolokolova (St.John's, NL)
  * Antonin Kucera (Prague)          * Oliver Kutz (Magdeburg)
  * Benedikt Loewe (Hamburg & Amsterdam)
  * Jack Lutz (Ames, IA)             * Florin Manea (Kiel)
  * Alberto Marcone (Udine)          * Radu Mardare (Aalborg)
  * Joe Miller (Madison, WI)
  * Russell Miller (Flushing, NY)    * Mia Minnes (La Jolla, CA)
  * Victor Mitrana (Bucharest, co-chair)
  * Ian Pratt-Hartmann (Manchester)  * Dag Normann (Oslo)
  * Mehrnoosh Sadrzadeh (London)     * Anne Smith (St Andrews)
  * Mariya Soskova (Sofia, co-chair) * Susan Stepney (York)
  * Paul Spirakis (Patras & Liverpool)
  * Jacobo Toran (Ulm)               * Marius Zimand (Towson, MD)

The PROGRAMME COMMITTEE cordially invites all researchers
(European and non-European) in computability related areas to
submit their papers (in PDF format, max 10 pages using the LNCS
style) for presentation at CiE 2015.

The submission site
is open.

For submission instructions consult

The CONFERENCE PROCEEDINGS will be published by LNCS, Springer


CiE 2015 http://fmi.unibuc.ro/CiE2015/

ASSOCIATION COMPUTABILITY IN EUROPE http://www.computability.org.uk
CiE Conference Series http://www.illc.uva.nl/CiE
CiE Membership Application Form http://www.lix.polytechnique.fr/CIE
Computability (Journal of CiE) http://www.computability.de/journal/
CiE on FaceBook https://www.facebook.com/AssnCiE
Association CiE on Twitter https://twitter.com/AssociationCiE

Michael Winter | 20 Oct 21:19 2014

CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

                           CALL FOR PAPERS

                  15th International Conference on
    Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

            28 September to 1 October 2015, Braga, Portugal
                  URL:  http://ramics2015.di.uminho.pt
         PDF: http://ramics2015.di.uminho.pt/RAMiCS15-CFP.pdf


 We invite submissions in the general area of Relational and Algebraic 
 Methods  in Computer Science. Special focus will lie on formal methods 
 for software engineering, logics of programs and links with neighbouring 

 Particular topics of interest for the conference cover,
 but are not limited to:

 * Algebraic approaches to
   - specification, development, verification, and analysis of programs
     and algorithms
   - computational logic, in particular logics of programs, modal and
     dynamic logics, interval and temporal logics
   - semantics of programming languages

 * Applications in fields such as
   - relational formal methods such as B or Z, tabular methods
   - information systems
   - graph theory and combinatorial optimisation
   - games, automata and language theory
   - spatio-temporal reasoning, knowledge acquisition
   - preference and scaling methods, computational social choice,
     social software

 * Theoretical foundations and supporting tools, including
   - mechanised and automated reasoning, decision procedures
   - process algebras, fixed point calculi, idempotent semirings,
     quantales, allegories
   - dynamic algebras, cylindric algebras and their applications in 


 Since 1994, the RelMiCS meetings on Relational Methods in Computer 
 Science have been a main forum for researchers who use the calculus of 
 relations and similar algebraic formalisms as methodological and 
 conceptual tools. The AKA workshop series on Applications of Kleene 
 algebra started with a Dagstuhl seminar in 2001 and was co-organised 
 with the RelMiCS conference until 2009. Since 2011, joint RAMiCS 
 conferences continue to encompass the scope of both RelMiCS and AKA.

 The predecessors of this conference were held in Dagstuhl (January 
 1994), Parati (September 1995), Hammamet (January 1997), Warsaw 
 (September 1998), Quebec (January 2000), Dagstuhl (February 2001), 
 Oisterwijk (October 2001), Malente (April 2003), St. Catharines 
 (January 2005), Manchester (September 2006), Frauenwoerth (April 2008), 
 Doha (November 2009), Rotterdam (June 2011), Cambridge UK (September 
 2012) and Marienstatt im Westerwald (April 2014).

 Student Program

 The conference will be accompanied by a PhD training program. Details 
 will be published in due time in a special call and on the conference 

 Proceedings and Submission

 All papers will be formally reviewed. We plan to publish the
 proceedings in the series Lecture Notes in Computer Science ready at
 the conference. Submissions must be in English, in Postscript or PDF
 format, and provide sufficient information to judge their merits.
 They must be unpublished and not submitted for publication elsewhere. 
 They should not exceed 16 pages in Springer LNCS style (accepted
 papers must be produced with LaTeX). Additional material may be
 provided by a clearly marked appendix or a reference to a manuscript
 on a website. This may be considered at the discretion of the PC.
 Deviation from these requirements may cause immediate rejection.
 One author of each accepted paper is expected to present the paper
 at the conference.

 Submission is via EasyChair at the following address:
 Formatting instructions and the LNCS styled files can be obtained via:

 As for the earlier conferences of this series, it is also intended to
 publish a selection of the best papers in revised and extended form in
 a special issue of the Journal of Logic and Algebraic Methods in
 Programming (JLAMP).

 Important Dates

     Title and abstract submission:                 March 18 2015
     Submission of full papers:                     March 26 2015
     Notification:                                  June  05 2015
     Final versions due (firm deadline):            July  10 2015

     Conference:                   September 28 - October 01 2015

 Programme Committee

     Rudolf Berghammer     (Kiel, Germany)
     Jules Desharnais      (Laval U., Canada)
     Marcelo Frias         (Buenos Aires, Argentina)
     Stephen Givant        (Mills College, USA)
     Hitoshi Furusawa      (Kagoshima, Japan)
     Timothy G. Griffin    (Cambridge, UK)
     Walter Guttmann       (Canterbury, New Zealand)
     Robin Hirsch          (London, UK)
     Peter Hoefner         (NICTA, Australia; Publicity chair)
     Ali Jaoua             (Doha, Qatar)
     Peter Jipsen          (Chapman U., USA)
     Wolfram Kahl          (McMaster U., Canada)
     Rodger Maddux         (Iowa State U., USA)
     Ali Mili              (NJIT, U. Heights, USA)
     Bernhard Moeller      (U. Augsburg, Germany)
     Martin E. Mueller     (U. Augsburg, Germany)
     Jose N. Oliveira      (U. Minho, Portugal; General chair)
     Ewa Orlowska          (Warsaw, Poland)
     Agnieszka Rusinowska  (Univ. Paris 1, France)
     Gunther Schmidt       (Munich, Germany)
     Renate Schmidt        (Manchester, UK)
     Isar Stubbe           (U. Littoral-Cote-d'Opale, France)
     Michael Winter        (Brock U., Canada; PC chair)


 Steering Committee

     Rudolf Berghammer  (Kiel, Germany)
     Jules Desharnais   (Laval U., Canada)
     Ali Jaoua          (Doha, Qatar)
     Peter Jipsen       (Chapman U., USA)
     Bernhard Moeller   (U. Augsburg, Germany)
     Jose N. Oliveira   (U. Minho, Portugal)
     Ewa Orlowska       (Warsaw, Poland)
     Gunther Schmidt    (Munich, Germany)
     Michael Winter     (Brock U., Canada)


 Organising Committee

     Jose N. Oliveira    (U. Minho, Portugal; General chair)
     Michael Winter      (Brock U., Canada; PC chair)
     Luis S. Barbosa     (U. Minho, Portugal)
     Manuel A. Cunha     (U. Minho, Portugal)
     Antonio N. Ribeiro  (U. Minho, Portugal)

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
Ramana Kumar | 16 Oct 18:18 2014

Theorems Produced by Type Definitions

Hi all,

There has been an interesting discussion on the OpenTheory mailing list recently regarding how to simplify the two theorems produced by a type definition in HOL Light and remove their free variables. The latest message in the thread, which shows the  suggestions by Mario Carneiro can be found here: http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html.

I'm cross-posting to this list because I think using Mario's suggestions would be an improvement to both HOL Light and Opentheory. I hope the respective authors of those systems might agree and implement the changes, and that anyone else with an interest might voice their opinion.

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Geoff Sutcliffe | 15 Oct 14:34 2014

CADE-25 Call for Papers, etc.



25th International Conference on Automated Deduction (CADE-25)
Berlin, Germany, 1-7 August 2015


Submission deadlines:

   14 November 2014 (workshops/tutorials/competitions)
16/23 February 2015 (papers)

CADE is the major international forum at which research on all aspects of
automated deduction is presented. The 25th jubilee edition will feature
a special session on the past, present, and future of automated deduction

  Ursula Martin      University of Oxford
  Frank Pfenning     Carnegie Mellon University
  David Plaisted     University of North Carolina at Chapel Hill
  Andrei Voronkov    University of Manchester

as invited speakers. In addition, there will be invited presentations by

  Ulrich Furbach     University of Koblenz
  Edward Zalta       Stanford University


Workshop proposals for CADE-25 are solicited. Both well-established
workshops and newer ones are encouraged. Similarly, proposals for workshops
with a tight focus on a core automated reasoning specialization, as well as
those with a broader, more applied focus, are very welcome.

Please provide the following information in your application document:

+ Workshop title.
+ Names and affiliations of organizers.
+ Proposed workshop duration (from half a day to two days) and preferred
+ Brief description of the goals and the scope of the workshop. Why is the
  workshop relevant for CADE?
+ Is the workshop new or has it met previously? In the latter case
  information on previous meetings should be given (e.g., links to the
  program, number of submissions, number of participants).
+ What are the plans for publication?


Tutorial proposals for CADE-25 are solicited. Tutorials are expected to be
half-day events, with a theoretical or applied focus, on a topic of interest
for CADE-25. Proposals should provide the following information:

+ Tutorial title.
+ Names and affiliations of organizers.
+ Brief description of the tutorial's goals and topics to be covered.
+ Whether or not a version of the tutorial has been given previously.

CADE will take care of printing and distributing notes for tutorials that
would like this service.


The CADE ATP System Competition (CASC), which evaluates automated theorem
proving systems for classical logics, has become an integral part of the
CADE conferences.

Further system competition proposals are solicited. The goal is to foster
the development of automated reasoning systems in all areas relevant for
automated deduction in a broader sense. Proposals should include the
following information:

+ Competition title.
+ Names and affiliations of organizers.
+ Duration and schedule of the competition.
+ Room/space requirements.
+ Description of the competition task and the evaluation procedure.
+ Is the competition new or has it been organized before?
  In the latter case information on previous competitions should be given.
+ What computing resources are required and how will they be provided?


High-quality submissions on the general topic of automated deduction,
including foundations, applications, implementations, and practical
experiences are solicited.

* Logics of interest include propositional, first-order, equational,
  higher-order, classical, description, modal, temporal, many-valued,
  constructive, other non-classical, meta-logics, logical frameworks, type
  theory, set theory, as well as any combination thereof.

* Paradigms of interest include theorem proving, model building, constraint
  solving, computer algebra, model checking, proof checking, and their

* Methods of interest include resolution, superposition, completion,
  saturation, term rewriting, decision procedures, model elimination,
  connection methods, tableaux, sequent calculi, natural deduction, as
  well as their supporting algorithms and data structures, including
  matching, unification, orderings, induction, indexing techniques, proof
  presentation and explanation, proof planning.

* Applications of interest include program analysis, verification and
  synthesis of software and hardware, formal methods, computational logic,
  computer mathematics, natural language processing, computational
  linguistics, knowledge representation, ontology reasoning, deductive
  databases, declarative programming, robotics, planning, and other areas
  of AI.

Submissions can be made in the categories regular papers and system
descriptions. The page limit in Springer LNCS style is 15 pages for regular
papers and 10 pages for system descriptions. Submissions must be unpublished
and not submitted for publication elsewhere. They will be judged on
relevance, originality, significance, correctness, and readability. System
descriptions should contain a link to a working system and will also be
judged on usefulness and design. Proofs of theoretical results that do not
fit in the page limit, executables of systems, and input data of experiments
should be made available, via a reference to a website or in an appendix of
the paper. Reviewers will be encouraged to consider this additional
material, but submissions must be self-contained within the respective page
limit; considering the additional material should not be necessary to
assess the merits of a submission. The proceedings of the conference will
be published in the Springer LNCS/LNAI series. Formatting instructions and
the LNCS style files can be obtained at 


At every CADE conference the Program Committee selects one of the
accepted papers to receive the CADE Best Paper Award. The award
recognizes a paper that the Program Committee collegially evaluates as
the best in terms of originality and significance, having substantial
confidence in its correctness. Overall technical quality,
completeness, scholarly accuracy, and readability are also
considered. Characteristics associated with a best paper include, for
instance, introduction of a strong new technique or approach, solution
of a long-standing open problem, introduction and solution of an
interesting and important new problem, highly innovative application
of known ideas or existing techniques, and presentation of a new
system of outstanding power. Under exceptional circumstances, the
Program Committee may give two awards (ex aequo) or give no award.

At CADE-25 we also intend to award the best student paper (details
will follow).


Workshop/Tutorials/System Competitions:

Submission deadline:      14 November 2014
Notification:             28 November 2014


Abstract deadline:        16 February 2015
Submission deadline:      23 February 2015
Rebuttal phase:           15-18 April 2015
Notification:             26 April 2015
Final version:            17 May 2015

Workshops and Tutorials:  1 August to 3 August (morning) 2015
Competitions:             1 to 7 August 2015
Conference:               3 August (afternoon) to 7 August 2015


Proposals for workshops, tutorials, and system competitions should be
uploaded via


Papers should be submitted via



Conference Chair:
  Christoph Benzmüller   Freie Universität Berlin

Program Committee Co-Chairs:
  Amy Felty              University of Ottawa
  Aart Middeldorp        University of Innsbruck

Workshop, Tutorial, and Competition Co-Chairs:
  Jasmin Blanchette      Technische Universität München
  Andrew Reynolds        EPFL Lausanne

Publicity and Web Chair:
  Julian Röder           Freie Universität Berlin

Program Committee
  Carlos Areces          Universidad Nacional de Córdoba
  Alessandro Armando     University of Genova
  Christoph Benzmüller   Freie Universität Berlin
  Josh Berdine           Microsoft Research
  Jasmin Blanchette      Technische Universität München
  Marta Cialdea Mayer    Universita di Roma Tre
  Stephanie Delaune      CNRS
  Gilles Dowek           Inria
  Amy Felty              University of Ottawa
  Reiner Hähnle          Technical University of Darmstadt
  Stefan Hetzl           Vienna University of Technology
  Marijn Heule           The University of Texas at Austin
  Nao Hirokawa           JAIST
  Ullrich Hustadt        University of Liverpool
  Deepak Kapur           University of New Mexico
  Gerwin Klein           NICTA and UNSW
  Laura Kovács           Chalmers University of Technology
  Carsten Lutz           Universität Bremen
  Assia Mahboubi         Inria
  Aart Middeldorp        University of Innsbruck
  Albert Oliveras        Technical University of Catalonia
  Nicolas Peltier        CNRS
  Brigitte Pientka       McGill University
  Ruzica Piskac          Yale University
  André Platzer          Carnegie Mellon University
  Andrew Reynolds        EPFL Lausanne
  Christophe Ringeissen  LORIA-INRIA
  Renate Schmidt         University of Manchester
  Stephan Schulz         DHBW Stuttgart
  Georg Struth           University of Sheffield
  Geoff Sutcliffe        University of Miami
  Alwen Tiu              Nanyang Technological University
  Freek Wiedijk          Radboud University Nijmegen

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Geoff Sutcliffe | 13 Oct 18:44 2014

NETYS 2015 Call for Papers


**NETYS 2015**
**May 13-15, 2015, AGADIR, MOROCCO**

*Aim and Scope:**
NETYS aims to bring together researchers and engineers from both the 
theory and practice of distributed and networked systems. The scope of 
the conference covers all aspects related to the design and the 
development of these systems, including, but not restricted to, 
multi-core architectures, concurrent and distributed algorithms, 
parallel/concurrent/distributed programming, distributed databases, 
cloud systems, networks, security, formal verification, etc.

NETYS will provide a forum to report on best practices and novel 
algorithms, results and techniques on networked systems. Original 
contributions as well as experience papers on the principles, design, 
implementation, modeling, analysis, verification, and application of 
networked systems are solicited. Specific concepts common to different 
forms of such systems are most welcome.

NETYS is coupled with the METIS Spring School which aims at introducing 
young researchers to the domain of distributed and networked systems 
through tutorials on basics, as well as lectures on new research topics 
and current trends in this domain.

*Paper submission:**
Submissions should contain original research and sufficient detail to 
assess the merits and relevance of the contribution. NETYS welcomes 
papers on theory, case studies and comparisons with existing 
experimental research, tools, as well as combinations of new theory with 
experimental evaluation.

NETYS is soliciting two forms of papers: full and short papers. Full 
papers are allowed a maximum of 15 pages in Springer's LNCS format, 
whereas short papers are allowed a maximum of 5 pages (in the same 
format), both in the submission and in the proceedings. A full paper 
submission might be accepted as such, as a short paper or a poster. A 
short paper may be accepted as such or as a poster.

Posters will be presented at the conference to reflect work in progress 
and will not lead to a publication in the proceedings. Authors are given 
the option to accept or not the type in which their paper is selected 
for acceptance.


Springer's Lecture Notes in Computer Science series will publish the 
proceedings of the conference (www.springer.com/lncs). It is required 
that each accepted paper be presented at the conference by one of its 

The Computing Journal could publish extended versions of selected papers 

Awards will be given to the best paper and the best student paper. A 
paper is eligible for the best student paper award if at least one of 
its authors is a full-time student at the time of submission. This 
should be indicated in the submission.

*Submission instructions:*

All submissions should follow the LNCS template. Submitted papers must 
be written in English. Full papers are allowed a maximum of 15 pages in 
LNCS format, whereas short papers are allowed a maximum of 5 pages, both 
in the submission and in the proceedings. Papers exceeding these limits 
may be rejected without review.

Paper submission will be handled by EasyChair, so please make sure that 
you have an active account. The papers must be submitted electronically at:

*Important dates**
- Abstract submission deadline: January 5, 2015
- Paper submission deadline: January 9, 2015
- Acceptance notification: March 9, 2015
- Camera ready copy due: April 10, 2015
- Conference: May 13-15, 2015


/_General Co-chairs_:/
Mohammed Erradi        ENSIAS, Rabat, Morocco
Rachid Guerraoui       EPFL, Switzerland

/_Program Co-chairs_:/
Ahmed Bouajjani        Univ. Paris Diderot, France
Hugues Fauconnier      Univ. Paris Diderot, France

/_Program Committee_:/
Parosh Aziz Abdulla    Univ. Uppsala, Sweden
Joffroy Beauquier      Univ. Paris 11, France
Gregor Bochmann        Univ. Ottawa, Canada
Carole Delporte        Univ. Paris Diderot, France
Amr El Abbadi          UCSB, USA
Khaldoun El Agha       Univ. Paris 11, France
Mohamed El Koutbi      ENSIAS, Rabat, Morocco
Boualem Benatallah     Univ. New South Wales, Australia
Mohamed El Kamili      USMBA, Fes, Morocco
Bernd Freisleben       Univ. Marburg, Germany
Mohamed Gouda          Univ. Texas at Austin
Vincent Gramoli        Univ. Sydney, Australia
Seif Haridi            SICS, Sweden
Maurice Herlihy        Brown Univ., USA
Claude Jard            Univ. Nantes, France
Zahi Jarir             Univ. Cadi Ayyad, Morocco
Anne-Marie Kermarrec   INRIA, Rennes, France
Rupak Majumdar         MPI-SWS, Germany
Stephan Merz           INRIA, Nancy, France
Louise Moser           UCSB, USA
Hassan Mountassir      Univ. Franche-Comt?, France
Guevara Noubir         Northeastern Univ., USA
Andreas Podelski       Univ. Freiburg, Germany
Shaz Qadeer            Microsoft Research, USA
Vivien Quema           INPG, Grenoble, France
Sergio Rajsbaum        UNAM, Mexico
Ganesan Ramalingam     Microsoft Research, India
Michel Raynal          IRISA, Rennes, France
Alexander Shvartsman   Univ. Connecticut, USA
Sebastian Tixeuil      Univ. Pierre et Marie Curie, France
Martin Vechev          ETH Zurich, Switzerland

_/Organizing Committee/_:
Khadija Bakkouch       IRFC, Rabat
Abdellah Boulouz       Univ. Ibn zohr, Agadir
Mohammed Erradi        ENSIAS, UM5S, Rabat
Zahi Jarir             Univ. Cadi Ayyad, Marrakech
Mohammed Ouzzif        ESTC, UH2M, Casablanca

_/Students Committee/_:
Meryeme Ayache        ENSIAS, UM5S, Rabat
Yahya Benkaouz        ENSIAS, UM5S, Rabat

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
Sophie Tison | 13 Oct 08:17 2014

RTA 2015 - First Call For Papers

              RTA 2015 - CALL FOR PAPERS 
           26th International Conference on
        29 June - 1 July, 2015, Warsaw, Poland 
      co-located with TLCA, as part of RDP 2015

RTA is the major forum for the presentation of research on all 
aspects of rewriting.  Topics of interest include:

* Foundations: string, term, net and graph rewriting; higher-order
rewriting; binding techniques; constrained rewriting and deduction;
categorical and infinitary rewriting; stochastic rewriting;
higher-dimensional rewriting; tree automata; confluence; 
termination; complexity; modularity; equational logic; 
universal algebra; rewriting logic; rewriting calculi.

* Algorithmic aspects and implementation: strategies; matching;
unification; anti-unification; narrowing; completion; parallel
execution; certification of rewriting properties; abstract machines;
automated (non)termination and confluence provers; automated
complexity analysis; system descriptions.

* Applications of rewriting: programming languages (functional, 
logic, object-oriented and other programming paradigms); type 
systems; program analysis, transformation and optimisation; 
rewriting models of programs; semantics; process calculi; 
functional calculi; explicit substitution; constraint solving; 
symbolic and algebraic computation; theorem proving; 
proof checking; system modelling; system synthesis and 
verification; XML queries and transformations; cryptographic 
protocols; security policies; systems biology; linguistics; 
rewriting in education.

Important Dates:
# Submission: title and abstract: 30 January 2015
              full paper: 6 February 2015
# Rebuttal period: 19-21 March 2015  
# Notification:    8 April 2015
# Final version:  25 April 2015

Submission and publication:
The RTA 2015 proceedings will be published by LIPIcs (Leibniz
International Proceedings in Informatics). Papers should present
original work, and should be submitted via Easychair:
Papers should be at most 15 pages (10 for system descriptions) 
in the style described in:
This year we particularly welcome submissions on applications of
rewriting. Application papers are regular papers (15 pages); their
originality is judged based on the novelty of the application or the
depth of the rewriting methods applied. 
System description papers present new software tools in which 
rewriting plays an important role, or significantly new versions 
of such tools. The paper should also include an evaluation of the 

Programme Committee:
M. Ayala-Rincon, U. Brasilia
H. Cirstea, Loria Nancy
S. Delaune, ENS Cachan
A. Di Pierro, U. Verona
G. Dowek, Inria
M. Fernandez, KCL, chair
J. Giesl, RWTH Aachen U.
M. Hanus, CAU Kiel
D. Kesner, U. Paris-Diderot
T. Kutsia, Johannes Kepler U. Linz
J. Levy, IIIA-CSIC Barcelona
S. Lucas, Polytechnic U. Valencia
C. Lynch, Clarkson U.
I. Mackie, E. Polytechnique
G. Moser, U. Innsbruck
D. Plump, U. York
F. van Raamsdonk, VU Amsterdam
K. Rose, Two Sigma, US
M. Sakai, Nagoya U.
A. Scedrov, U. Pennsylvania
M. Schmidt-Schauss, U. Frankfurt
C. Schuermann, ITU Copenhagen	
P. Selinger, Dalhousie U.
P. Severi, U. Leicester
K. Ueda, Waseda U.

Conference Chair:
Aleksy Schubert
Warsaw University

For more information, please contact the PC chair:
Maribel.Fernandez <at> kcl.ac.uk

Pr. Sophie Tison (RTA publicity chair)
LIFL - University of Lille- CNRS
sophie.tison <at> lifl.fr

Attachment (smime.p7s): application/pkcs7-signature, 3818 bytes
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
hol-info mailing list
hol-info <at> lists.sourceforge.net
Ramana Kumar | 11 Oct 11:11 2014

annotation with HOLKeyword

When I make a munger with monadsyntax and use it to typeset some monadic functions, the "do" and "od" delimiters of a list of binds are emitted as-is. I would like them to be annotated as HOLKeywords.

I know I could probably use the override map for that, but it seems like there ought to be a more proper way of doing it. How do keywords (like "if") normally get annotated, and can we do the same for "do" and "od"?
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
hol-info mailing list
hol-info <at> lists.sourceforge.net
Marjan Sirjani | 7 Oct 00:02 2014

Final CFP: FSEN 2015

Our apologies if you have received multiple copies.

                                                                    FSEN  2015: CALL FOR PAPERS
Sixth International Conference on
Fundamentals of Software Engineering 2015 Theory and Practice (FSEN '15)
Tehran, Iran
22 - 24 April, 2015
-- About FSEN --
FSEN is an international conference that aims to bring together researchers, engineers, developers,
and practitioners from the academia and the industry to present and discuss their research work in
the area of formal methods for software engineering. This conference seeks to facilitate the transfer
of experience, adaptation of methods, and where possible, foster collaboration among different groups.
The topics of interest cover all aspects of formal methods, especially those related to advancing
the application of formal methods in the software industry and promoting their integration with
practical engineering techniques.
-- Important Dates --
Abstract Submission: October 24, 2014
Paper Submission: October 31, 2014
Notification: December 26, 2014
Camera Ready: January 16, 2015
Conference: April 22-24, 2015
-- Keynote Speakers --
 Holger Giese, Hasso Plattner Institute, Germany
 John Hughes, Chalmers University of Technology, Sweden
 Paola Inverardi, University of L'Aquila, Italy
-- Topics of Interest --
The topics of this conference include, but are not restricted to, the following:
* Models of programs and software systems
* Software specification, validation, and verification
* Software testing
* Software architectures and their description languages
* Object and multi-agent systems
* Coordination and feature interaction
* Integration of formal and informal methods
* Integration of different formal methods
* Component-based and Service-oriented software systems
* Self-adaptive software systems
* Model checking and theorem proving
* Software and hardware verification
* CASE tools and tool integration
* Industrial Applications
-- Paper Submission --
Papers should be formatted according to the Springer LNCS style,
not exceed 15 pages (including figures and references), submitted in PDF or postscript format,
and not be submitted simultaneously for publication elsewhere.
Papers will be evaluated based on originality, significance, relevance, correctness and clarity.
-- Proceedings and Special Issues --
The post-proceedings of FSEN'15 will be published by Springer Verlag in the LNCS series
(official approval in process). There will also be a pre-proceeding, printed locally by IPM,
available at the conference. Following the tradition of the past editions,
we plan to have a special issue of Science of Computer Programming journal devoted to FSEN'15 (to be confirmed).
-- General Chair --
 Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
 Hamid Sarbazi-azad - IPM, Iran; Sharif University of Technology, Iran
-- Program Chairs --
 Mehdi Dastani - Utrecht University, The Netherlands
 Marjan Sirjani - Reykjavík University, Iceland; University of Tehran, Iran
-- Publicity Chair --
 Hossein Hojjat - Cornell University, USA
-- Steering Committee --
 Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
 Christel Baier - University of Dresden, Germany
 Frank de Boer - CWI, Netherlands; Leiden University, Netherlands
 Ali Movaghar - IPM, Iran; Sharif University of Technology, Iran
 Hamid Sarbazi-azad - IPM, Iran; Sharif University of Technology, Iran
 Marjan Sirjani - Reykjavik University, Iceland; University of Tehran, Iran (chair)
 Jan Rutten - CWI, Netherlands; Vrije University Amsterdam, Netherlands
-- Program Committee --
 Mohammad Abdollahi Azgomi - Iran University of Science and Technology, Iran
 Christel Baier - TU Dresden, Germany
 Ezio Bartocci, Vienna University of Technology, Austria
 Borzoo Bonakdarpour - University of Waterloo, Canada
 Marcello Bonsangue - Leiden University, Netherlands
 Mario Bravetti - University of Bologna, Italy
 Fabiano Dalpiaz - Utrecht University, Netherlands
 Mehdi Dastani - Utrecht University, Netherlands
 Erik De Vink - Technical University of Eindhoven, Netherlands
 Klaus Dräger - University of Oxford, UK
 Wan Fokkink - Vrije Universiteit Amsterdam, Netherlands
 Masahiro Fujita - University of Tokyo, Japan
 Maurizio Gabbrielli - University of Bologna, Italy
 Fatemeh Ghassemi - University of Tehran, Iran
 Jan Friso Groote - Technical University of Eindhoven, Netherlands
 Hassan Haghighi - Shahid Beheshti University, Iran
 Hossein Hojjat - Cornell University, USA
 Mohammad Izadi - Sharif University of Technology, Iran
 Mohammad Mahdi Jaghoori - CWI, Netherlands; Academic Medical Center of University of Amsterdam, Netherlands
 Einar Broch Johnsen - University of Oslo, Norway
 Joost-Pieter Katoen - RWTH Aachen University, Germany
 Narges Khakpour - KTH, Sweden
 Ramtin Khosravi - University of Tehran, Iran
 Zhiming Liu - Birmingham City University, UK
 Seyyed Hassan Mirian Hosseinabadi - Sharif University of Technology, Iran
 Ugo Montanari - University of Pisa, Italy
 Peter Mosses - Swansea University, UK
 Mohammad Reza Mousavi - Halmstad University, Sweden
 Ali Movaghar - Sharif University of Technology, Iran
 Peter Olveczky - University of Oslo, Norway
 Jose Proenca - K.U.Leuven, Belgium
 Niloofar Razavi - University of Toronto, Canada
 Philipp Ruemmer - Uppsala University, Sweden
 Gwen Salaun - Grenoble INP, Inria, France
 Cesar Sanchez - IMDEA Software Institute, Spain
 Wendelin Serwe - INRIA, France
 Marjan Sirjani - Reykjavik University, Iceland
 Meng Sun - Peking University, China
 Carolyn Talcott - SRI International, USA
 Samira Tasharofi - Microsoft, USA
 Tayssir Touili - LIAFA, France
 Danny Weyns - Linnaeus University, Sweden
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
hol-info mailing list
hol-info <at> lists.sourceforge.net
DIFTS14 | 7 Oct 15:26 2014

DIFTS'14 - Call For Participation

                      CALL FOR PARTICIPATION

Third International Workshop on Design and Implementation
of Formal Tools
and Systems (co-located with FMCAD 2014, and MEMOCODE


Lausanne, Switzerland
October 20, 2014


DIFTS (Design and Implementation of Formal Tools and
Systems) workshop
emphasizes insightful experiences in formal tools and
systems design.  It
provides a forum for sharing challenges and solutions that
are original with
ground breaking results.

Often the design and implementation of tools for formal
analysis require
non-trivial engineering decisions. Many challenges are
faced, which often can
only be met with ingenious implementation techniques.
These techniques actually
play a crucial role in making the idea work in practice.
The workshop provides
an opportunity for discussing engineering aspects and
various design decisions
required to put such formal tools and systems into
practical use.




Rolf Drechsler, University of Bremen, Germany
"Coverage at the Formal Specification Level"

Wolfgang Kunz, University of Kaiserslautern, Germany
"The big hurdles for FV tools in industrial practice – can
we overcome them insystem-level design flows?"

Fahim Rahim, Atrenta, France
"Efficiently using formal verification techniques to
reduce power"

REGISTRATION (provided through FMCAD'14 website)

Registration information is available at

A list of recommended hotels with preferential rates is
available at



Malay K. Ganai, Atrenta, USA
Gianpiero Cabodi, Politecnico di Torino, Italy


Chao Wang, Virginia Tech, USA
Shuvendu Lahiri, Microsoft Research, USA
Roberto Bruttomesso, Atrenta, France
Alberto Griggio, FBK-IRST, Italy
Alper Sen, Bogazici University, Turkey
Joao Marques-Silva, University College Dublin, Ireland
Priyank Kalla, University of Utah, USA
Supratik Chakraborty, IIT Bombay, India
Erika Abraham, RWTH Aachen University, Germany
Andreas Veneris, University of Toronto, Canada
Daniel Grosse, University of Bremen, Germany


Pasini Paolo, Politecnico di Torino, Italy
Marco Palena, Politecnico di Torino, Italy

Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer