Cyber Security Symposium 2015 Call for Papers

I apologize if you receive multiple copies of this.

-jimaf

 

=====================================================================================

CALL FOR ABSTRACTS

Cyber Security Symposium: Your Security, Your Future

=====================================================================================

 

April 7-8, 2015 - - - Coeur d’Alene, Idaho, U.S.A.

 

http://www.cybersecuritysymposium.com

 

Key Dates

Abstract Submission Deadline: January 16, 2015

Presenter Notification: February 3, 2015

Early Registration Deadline: February 6, 2015

 

Introduction

The 2015 Cyber Security Symposium is an opportunity for academic researchers from all disciplines, software developers, and system developers from industry and government to meet and discuss state-of-the-art and state-of-the-practice research, technologies, and processes related to cyber security.  The symposium seeks submissions from academia, industry and government presenting novel research, case studies, and best practices on all practical and theoretical aspects of cyber security.

 

We are interested in presentations and papers with topics including, but not limited to:

·                   Network Security

·                   Secure Coding Practices

·                   Software Analysis

·                   Security Policies

·                   Economic Impacts of Security

·                   Privacy

·                   Sociological and Human Factor Aspects of Security

·                   Critical Infrastructure Security

·                   Transportation System Security

·                   Power grid/Smart Grid security

·                   System Security Case Studies

 

Electronic Submission

Abstract submissions up to 500 words in length are being accepted at this time.  To submit your abstract, please go to the submission site at: https://www.easychair.org/conferences/?conf=cybersec15

 

Each abstract submission should be submitted with an understanding that, if accepted, at least one of the authors must attend the conference to present the work.

 

All authors of accepted abstracts will be given the opportunity to submit full research papers (up to 10 pages) and extended abstracts (up to 4 pages) in the form of position papers, discussions of new technologies from industry, and discussions of current hot topics/needs in cyber security to be considered for future publication in a Springer Verlag publication. 

------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Mahdi Jaghoori | 12 Dec 20:57 2014
Picon
Picon

Call for papers TTCS'15 (Tehran, Iran)


(apologies if you receive multiple copies)

=========================================
Topics in Theoretical Computer Science (TTCS 2015)
http://www.ttcs.ir/
Institute for Research in Fundamental Sciences (IPM), Tehran, Iran
August 26-28, 2015
=========================================

Scope

TTCS is a new bi-annual conference series, intending to serve as a forum for novel and high-quality research in all areas of Theoretical Computer Science. The conference is held in cooperation with the European Association for Theoretical Computer Science. 

There will be a number of satellite events at TTCS, These will feature presentation of early research results, and position papers. There will also be a forum for Ph.D. students to receive comments about their ongoing research projects.

Topics of interest include but are not limited to:

  • algebra and co-algebra in computer science,
  • algorithms and data structures,
  • algorithmic coding theory,
  • algorithmic graph theory and combinatorics,
  • approximation algorithms,
  • computational complexity,
  • computational geometry,
  • computational learning theory,
  • concurrency theory,
  • coordination languages,
  • economics and algorithmic game theory,
  • fixed parameter algorithms,
  • formal verification and model-based testing,
  • logic in computer science,
  • machine learning
  • methods, models of computation and reasoning for embedded, hybrid, and cyber-physical systems,
  • optimization,
  • parallel and distributed algorithms,
  • quantum computing,
  • randomness in computing,
  • stochastic and probabilistic specification and reasoning
  • theoretical aspects of other CS-related research areas, e.g., computational science, databases, information retrieval, and networking,
  • theoretical cryptography,
  • theory of programming languages, and
  • type theory and its application in program verification.
Anuj Dawar, Cambridge University, UK 
Michael Fellows, Charles Darwin University, Australia 
Mehrnoosh Sadrezadeh, Queen Mary University of London, UK 

Submission

For the main conference, we solicit research papers in all areas of theoretical computer science. All papers will undergo a rigorous review process and will be judged based on their originality, soundness, significance of the results, and relevance to the theme of the conference.

Papers should be written in English. Research papers should not exceed 15 pages in the LNCS style format. Multiple and/or concurrent submission to other scientific venues is not allowed and will result in rejection as well as notification to the other venue. Any case of plagiarism (including self-plagiarism from earlier publications) will result in rejection as well as notification to the the authors' institutions.

Papers should be submitted through our EasyChair submission website: https://www.easychair.org/conferences/?conf=ttcs2015 . The web site is open for submissions.

Important Dates

  • Paper Submission: May 15, 2015 (Anywhwere on Earth)
  • Author notification: June 26, 2015
  • Camera ready paper due: July 10, 2015
  • Conference: August 26-28, 2015

Program Committee

Track A: Algorithms and ComplexityTrack B: Logic, Semantics, and Programming Theory



------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Andrzej Murawski | 14 Dec 23:52 2014
Picon
Picon

LICS 2015 - Last Call for Papers

                         CALL FOR PAPERS

               Thirtieth Annual ACM/IEEE Symposium on
                 LOGIC IN COMPUTER SCIENCE (LICS)

                  July 6–10, 2015, Kyoto, Japan

                http://lics.rwth-aachen.de/lics15/

VENUE

LICS 2015 will be hosted in Kyoto, Japan during the week 6-10 July
2015 and will be colocated with ICALP 2015.

SCOPE

The LICS Symposium is an annual international forum on theoretical and
practical topics in computer science that relate to logic, broadly
construed. We invite submissions on topics that fit under that rubric.

Suggested, but not exclusive, topics of interest include: automata
theory, automated deduction, categorical models and logics,
concurrency and distributed computation, constraint programming,
constructive mathematics, database theory, decision procedures,
description logics, domain theory, finite model theory, formal aspects
of program analysis, formal methods, foundations of computability,
higher-order logic, lambda and combinatory calculi, linear logic,
logic in artificial intelligence, logic programming, logical aspects
of bioinformatics, logical aspects of computational complexity,
logical aspects of quantum computation, logical frameworks,  logics of
programs, modal and temporal logics, model checking, probabilistic
systems, process calculi, programming language semantics, proof
theory, real-time systems, reasoning about security and privacy,
rewriting, type systems and type theory, and verification.

IMPORTANT DATES

Authors are required to submit a paper title and a short abstract of
about 100 words in advance of submitting the extended abstract of the
paper. The exact deadline time on these dates is given by AoE
(anywhere on earth).

Titles & Short Abstracts Due:     January  12, 2015
Extended Abstracts  Due:           January 19, 2015
Author feedback/rebuttal period:  March 12-16, 2015
Author Notification:                 March 30, 2015
Final Versions Due for Proceedings:  April 27, 2015

Deadlines are firm; late submissions will not be considered. All
submissions will be electronic via
https://www.easychair.org/conferences/?conf=lics2015.

SUBMISSION INSTRUCTIONS

Every extended abstract must be submitted in the IEEE Proceedings
2-column 10pt format and may not be longer than 12 pages, including
references. LaTeX style files are available on the conference website.

The extended abstract must be in English and provide sufficient detail
to allow the program committee to assess the merits of the paper.  It
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 and to computer science, all phrased for
the non-specialist. Technical development directed to the specialist
should follow. References and comparisons with related work must be
included. (If necessary, detailed proofs of technical results may be
included in a clearly-labeled appendix, to be consulted at the
discretion of program committee members.) Extended abstracts not
conforming to the above requirements will be rejected without further
consideration. Paper selection will be merit-based, with no a priori
limit on the number of accepted papers. Papers authored or co-authored
by members of the program committee are not allowed.

Results must be unpublished and not submitted for publication
elsewhere, including the proceedings of other symposia or workshops.
The program chair must be informed, in advance of submission, of any
closely related work submitted or about to be submitted to a
conference or journal.

Authors of accepted papers are expected to sign copyright release
forms.  One author of each accepted paper is expected to present it at
the conference.

SHORT PRESENTATIONS

A session of short presentations, intended for descriptions of student
research, works in progress, and other brief communications, is
planned. These abstracts will not be published. Dates and guidelines
will be posted on the conference website.

KLEENE AWARD FOR BEST STUDENT PAPER

An award in honor of the late Stephen C. Kleene will be given for the
best student paper(s), as judged by the program committee.

SPECIAL ISSUES

Full versions of up to three accepted papers, to be selected by the
program committee, will be invited for submission to the Journal of
the ACM. Additional selected papers will be invited to a special issue
of Logical Methods in Computer Science.

SPONSORSHIP

The symposium is sponsored by ACM SIGLOG and the IEEE Technical
Committee on Mathematical Foundations of Computing, in cooperation
with the Association for Symbolic Logic and the European Association
for Theoretical Computer Science.

PROGRAM COMMITTEE CHAIR

Catuscia Palamidessi, INRIA & E. Polytechnique

PROGRAM COMMITTEE

Pablo Barceló, U. Chile
Gilles Barthe, IMDEA
Andrej Bauer, IMFM
Lev Beklemishev, Russian Ac. of Sci.
Patricia Bouyer-Decitre, CNRS & ENS Cachan
Adam Chlipala, MIT
Agata Ciabattoni, TU Wien
Véronique Cortier, CNRS Loria
Pedro D'Argenio, UN Cordoba
Anuj Dawar, U. Cambridge
Mariangiola Dezani, U. Torino
Yuxi Fu, SJTU
Rob van Glabbeek, NICTA
Ichiro Hasuo, U. Tokyo
Martin Hofmann, LMU
Delia Kesner, U. Paris Diderot
Barbara König, U. Duisburg-Essen
Laura Kovács, Chalmers UT
Dexter Kozen, Cornell U.
Manfred Kufleitner, U. Stuttgart
Anthony W. Lin, Yale-NUS College
Simone Martini, U. Bologna
Madhavan Mukund, Chennai Math. Inst.
Filip Murlak, U. Warsaw
Gopalan Nadathur, U. Minnesota
Frank Pfenning, CMU
Ian Pratt-Hartmann, U. Manchester
Albert Rubio, U. Barcelona
Peter Selinger, Dalhousie U.
Alessandra Silva, Radboud U.
Tachio Terauchi, JAIST
Ashish Tiwari, SRI
Bow-Yaw Wang, Academia Sinica

CONFERENCE CHAIR

Masahito Hasegawa, RIMS, Kyoto U.

WORKSHOP CHAIR

Patricia Bouyer-Decitre, CNRS & ENS Cachan

PUBLICITY CHAIR

Andrzej Murawski, University of Warwick

LICS ORGANIZING COMMITTEE

M. Abadi, L. Aceto, R. Alur, M. P. Bonacina, P. Bouyer-Decitre, K.
Chatterjee, A. Compagnoni, A. Dawar, N. Dershowitz, M. Fernandez, M.
Grohe, O. Grumberg, T. Henzinger, P. Kolaitis, O. Kupferman, B.
Larose, D. Miller, M. Mislove, A. Murawski, C. Palamidessi, L. Ong
(chair), P. Panangaden, K. Rose, A. Scedrov, D. Shmoys, M. Valeriote

------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Christian Urban | 12 Dec 16:54 2014
Picon

1st CFP for ITP 2015 in Nanjing


CALL FOR PAPERS: ITP 2015

The 6th International Conference on Interactive Theorem Proving

24 - 27 August 2015 in Nanjing, China

ITP is the premier international conference for researchers from all
areas of interactive theorem proving and its applications. It
represents the natural evolution of the TPHOLs conference series to
include research related to all other interactive theorem provers.

 *****************************************************
 *  http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/  *
 *****************************************************


Important Dates
---------------
Title & Abstract Submission:  9 March 2015
Full Paper Submission:       13 March 2015 
Author Notification:           15 May 2015
Camera-Ready Papers due:       5 June 2015
Conference:            24 - 27 August 2015

Topics
------

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, and
- concise and elegant worked examples of formalizations ("Proof Pearls").

Papers should be no more than 16 pages in length and are to be
submitted in PDF format. They must conform to the LNCS style
preferably using LaTeX. The proceedings are to be published as a
volume in the Lecture Notes in Computer Science series and will be
available to participants at the conference.

Authors of accepted papers are expected to present their paper at the
conference.

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.

Programme Committee
-------------------

Andrea Asperti       University of Bologna, Italy
Jesper Bengtson      IT University of Copenhagen, Denmark
Stefan Berghofer     Secunet Security Networks AG, Germany
Yves Bertot          INRIA, France
Lars Birkedal        Aarhus University, Denmark
Sandrine Blazy       University of Rennes, France
Bob Constable        Cornell University, USA
Thierry Coquand      University of Gothenburg, Sweden
Xinyu Feng           University of Science and Technology, China
Ruben Gamboa         University of Wyoming, USA
Herman Geuvers       Radboud University Nijmegen, The Netherlands
Mike Gordon          Cambridge University, United Kingdom
Elsa Gunter          University of Illinois, Urbana-Champaign, USA
John Harrison        Intel Corporation, USA
Hugo Herbelin        INRIA, France
Matt Kaufmann        University of Texas at Austin, USA
Gerwin Klein         NICTA, Australia
Cesar Munoz          NASA Langley Research Center, USA
Tobias Nipkow        TU München, Germany
Michael Norrish      NICTA, Australia
Scott Owens          University of Kent, United Kingdom
Randy Pollack        Havard University, USA
Carsten Schürmann    IT University of Copenhagen, Denmark
Konrad Slind         Rockwell Collins, USA
Alwen Tiu            Nanyang Technological University, Singapore
Christian Urban      King's College London, United Kingdom (co-chair)
Dimitrios Vytiniotis Microsoft Research Cambridge, United Kingdom
Xingyuan Zhang 	     PLA University of Science and Technology, China (co-chair)

Organizers
----------
Xingyuan Zhang 
Chunhan Wu 
Jinshang Wang 
Christian Urban

------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
Muhammad Qasim | 11 Dec 23:30 2014
Picon
Picon

WF_INDUCT_TAC for HOL4

Hello,

I am looking for an alternative of WF_INDUCT_TAC for HOL4. I would be  
greatful if someone can provide good advice. I found a link for this  
tactic but the code is for hol_light.

http://mws.cs.ru.nl/~mptp/hol-flyspeck/trunk/wf.html

Looking forward to your response. Thank you.

Regards

Qasim

------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
Geoff Sutcliffe | 10 Dec 14:33 2014
Picon

CICM Call for Papers


                              Call for Papers

                Conference on Intelligent Computer Mathematics
                                 CICM 2015

                              13-17 July 2015
                            Washington DC, USA

Digital and computational solutions are becoming the prevalent means for the
generation, communication, processing, storage and curation of mathematical
information. Separate communities have developed to investigate and build
computer based systems for computer algebra, automated deduction, and
mathematical publishing as well as novel user interfaces. While all of these
systems excel in their own right, their integration can lead to synergies
offering significant added value. The Conference on Intelligent Computer
Mathematics (CICM) offers a venue for discussing and developing solutions
to the great challenges posed by the integration of these diverse areas.

CICM has been held annually as a joint meeting since 2008, co-locating
related conferences and workshops to advance work in these
subjects. Previous meetings have been held in Birmingham (UK 2008),
Grand Bend (Canada 2009), Paris (France 2010), Bertinoro (Italy 2011),
Bremen (Germany 2012), Bath (UK 2013), and Coimbra (Portugal 2014).

This is a (short version of the) call for papers for CICM 2015, which
will be held in Washington, D.C., 13-17 July 2015.

The full version of the CFP is available from the conference web page at
http://cicm-conference.org/2015/cicm.php

**********************************************************************
The principal tracks of the conference will be:
**********************************************************************

* Calculemus (Symbolic Computation and Mechanised Reasoning)
  Chair: Jacques Carette
* DML (Digital Mathematical Libraries)
  Chair: Volker Sorge
* MKM (Mathematical Knowledge Management)
  Chair: Cezary Kaliszyk
* Systems and Data
  Chair: Florian Rabe

Publicity chair is Serge Autexier. The local arrangements will be
coordinated by the Local Arrangements Chairs, Bruce R. Miller
(National Institute of Standards and Technology, USA) and Abdou
Youssef (The George Washington University, Washington, D.C.), and the
overall programme will be organized by the General Programme Chair,
Manfred Kerber (U. Birmingham, UK).

As in previous years, it is anticipated that there will be a number
co-located workshops, including one to mentor doctoral students giving
presentations. We also solicit for project descriptions and
work-in-progress papers.

**********************************************************************
Important Dates
**********************************************************************

Conference submissions:
Abstract submission deadline:      16 February 2015
Submission deadline:               23 February 2015
Reviews sent to authors:            6 April    2015
Rebuttals due:                      9 April    2015
Notification of acceptance:        13 April    2015
Camera ready copies due:           27 April    2015
Conference:                     13-17 July     2015

Work-in-progress and Doctoral Programme submissions:
Submission deadline:
(Doctoral: Abstract+CV)             4 May      2015
Notification of acceptance:        25 May      2015
Camera ready copies due:            1 June     2015

------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
Rob Arthan | 7 Dec 19:49 2014

Controlling instantiation in rewriting

I am working on a paper about a proof procedure and realised that
I was about to write something rather specific to ProofPower.
In ProofPower, the rewriting conversions and tactics treat
free variables on the left-hand side of the equations you are
rewriting with as constants and will only instantiate them to a
variable of the same name. I believe that HOL4 and
HOL Light don’t do this, i.e., the rewriting functions in those
systems will happily instantiate free variables on the left-hand side
of the equations.

My question is this: how easy is it to code something like the
ProofPower behaviour in HOL4 or HOL Light? (The HOL4
documentation for REWR_CONV implies that you can prevent x
being instantiated by adding x = x to the assumptions of the
rewriting theorems and then eliminating it afterwards,
but I couldn’t work out whether that would also inhibit
type instantiation, which I wouldn’t want to do.)

If it makes any difference, I am specifically interested in rewriting
with Miller-Nipkow style higher-order matching rather than first-order
matching. I believe that the HOL Light rewriting functions all
use M-N style matching. I couldn’t figure out from the REWR_CONV
documentation what goes on in HOL4.

Regards,

Rob.
------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Scott Owens | 5 Dec 13:51 2014
Picon

Funded PhD studentship on verified compilers

I'm looking for a PhD student to work with me adding concurrency to the CakeML verified compiler in HOL4
(https://cakeml.org). The position is fully funded for students from the UK or EU. The application
deadline is 15 January, 2015.

http://www.jobs.ac.uk/job/AJW215/funded-phd-project-concurrent-cakeml/


Scott Owens
School of Computing
University of Kent
Canterbury, United Kingdom
------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Asad Ahmed | 3 Dec 11:23 2014
Picon

Type Checking issue

Hi

I am using Hol-light on Ubuntu 13.10, I need to know the code fragment or whatever the method is to invoke the type printing. There is code fragment in tutorial available at http://www.cl.cam.ac.uk/~jrh13/hol-light/,

---For Showing type ----)

 let print_typed_var tm =
      let s,ty = dest_var tm in
      print_string("("^s^":"^string_of_type ty^")") in
    install_user_printer("print_typed_var",print_typed_var);;

(--For deleting types -----)

delete_user_printer "print_typed_var";;

It works flawlessly on windows but it is not working in Ubuntu OS. 
When I run this on emacs23 shell it goes like this

#  let print_typed_var tm =
      let s,ty = dest_var tm in
      print_string("("^s^":"^string_of_type ty^")") in
    install_user_printer("print_typed_var",print_typed_var);;
      Characters 138-171:
      install_user_printer("print_typed_var",print_typed_var);;
                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type string * (term -> unit)
       but an expression was expected of type
         string * (Format.formatter -> term -> unit)
       Type term = Hol.term is not compatible with type Format.formatter 


Thanks in Advance
------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Serge Autexier | 2 Dec 19:11 2014
Picon

CICM 2015: Call for Workshops

                     Call for Workshop Proposals

     CICM 2015 - Conference on Intelligent Computer Mathematics
                           July 13-17, 2015
       The George Washington University, Washington, D.C , USA
                 http://www.cicm-conference.org/2015

----------------------------------------------------------------------

As   computers   and   communications  technology   advance,   greater
opportunities arise  for intelligent mathematical  computation.  While
computer  algebra, automated  deduction,  mathematical publishing  and
novel user interfaces individually have long and successful histories,
we are  now seeing  increasing opportunities  for synergy  among these
areas.  The Conference  on  Intelligent  Computer Mathematics  (CICM)
offer a venue for discussing these areas and their synergy.

CICM has been held annually as  a joint meeting since 2008, colocating
related conferences and  workshops to advance work  in these subjects.
Previous meetings have been held in Birmingham (U.K. 2008), Grand Bend
(Canada  2009), Paris  (France 2010),  Bertinoro (Italy  2011), Bremen
(Germany 2012), Bath (U.K. 2013) and Coimbra (Portugal, 2014).

This is a  call for proposals for  workshops to be held  at CICM 2015,
which will be held in Washington D.C. (USA), July 13-17 next year.

The principal tracks of the 2015 meeting will be

  Calculemus (Symbolic Computation and Mechanised Reasoning)
  DML (Towards a Digital Mathematics Library)
  MKM (Mathematical Knowledge Management)
  Systems and Data

Some of the workshops that have been held at past CICM meetings are:

  Automated Reasoning: Bridging the Gap between Theory and Practice
  Compact Computer Algebra
  Empirically Successful Automated Reasoning for Mathematics
  Intelligent Proof Search
  Mathematical user Interfaces
  OpenMath
  Pen-Based Mathematical Computation
  Programming languages for Mechanized Mathematics Systems
  SCIEnce
  The Notion of Proof

Proposals for workshops  to be held at CICM  2015 are solicited.  Both
well-established workshops and newer or brand new ones are encouraged.

Please provide the following information:

 + Workshop title.
 + Names and affiliations of organizers.
 + Brief description of workshop goals and/or topics.
 + Proposed workshop duration (half a day up to two days is possible).
 + If the workshop has met previously, please include the conference 
   affiliation for the previous meeting. If the workshop is new, 
   please indicate so.

CICM  will take  care  of copying  and  distributing informal  printed
proceedings for  workshops that  would like this  service, as  well as
permanently archived open access online proceedings with CEUR-WS.org.

All proposals should be sent via email to

             cicm-organizers <at> cs.bham.ac.uk

for consideration by the CICM 2015 organizers:

 Local Organization Chairs:    Bruce Miller    (NIST)
                               Abdou Youssef   (GWU, USA)
 General Program Chair:        Manfred Kerber  (U. Birmingham, UK)
 Calculemus Track Chair:       Jacques Carette (McMaster U., Canada)
 DML Track Chair:              Volker Sorge    (U. Birmingham, UK)
 MKM Track Chair:              Cezary Kaliszyk (U. Innsbruck, Austria)
 System & Data Chair:          Florian Rabe    (JUB, Germany)
 Workshop Chair:               Serge Autexier  (DFKI, Germany)

Important dates:

 Deadline for proposal submissions:                   January 23, 2015
 Acceptance/rejection notification:                   February 4, 2015
 Workshop dates:                                      July 13-17, 2015

----------------------------------------------------------------------

------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
David Sanán | 3 Dec 03:26 2014
Picon

printing double space in emacs

Hi all,
I recently changed my computer at home and reinstalled everything, including HOL4.But after the reinstall HOL output shows double empty lines, e.g.

 ITSET_IND;

val it =

   |- ∀P.


     (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒


     ∀v v1. P v v1:

   thm

which is a little bit annoying for me...

is it possible to adjust this somehow?

Many thanks,
David.
------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Gmane