YuHui Lin | 27 Mar 12:42 2015
Picon
Picon

AVoCS 2015: Second Call for Papers

---------------------------------------------------------------------
                      SECOND CALL FOR PAPERS

              The 15th International Workshop on 
          Automated Verification of Critical Systems 
                        AVoCS 2015

             1-4 September 2015, Edinburgh, UK

          https://sites.google.com/site/avocs15/
                avocs2015 <at> easychair.org
---------------------------------------------------------------------

IMPORTANT DATES
  Submission of abstract for full papers: 5th June 2015
  Submission of full papers: 12th June 2015
  Notification (full papers): 14th July 2015
  Submission of research idea papers: 7th August 2015
  Notification (research idea): 14th August 2015
  Early registration: 18th August 2015
  Submissions of final versions: 21st August 2015 

INVITED SPEAKERS
  Colin O'Halloran (D-RisQ & the University of Oxford)
  Don Sannella (Contemplate & the University of Edinburgh)

SPONSORS
  Formal Methods Europe (FME)
  The Scottish Informatics & Computer Science Alliance (SICSA)

(Continue reading)

alexander.perucci | 23 Mar 14:15 2015
Picon

FOCLASA 2015 - 2nd Call For Papers

[Apologies for multiple postings]

-- First Call for Papers --

FOCLASA 2015: 14th International Workshop on Foundations of
Coordination Languages and Self-Adaptive Systems

http://foclasa.lcc.uma.es/

5 September 2015, Madrid (Spain)
In conjunction with CONCUR 2015
==============================================================

FOCLASA 2015 is a workshop colocated with the 25th International
Conference on Concurrency Theory (CONCUR 2015 -
http://mafalda.fdi.ucm.es/concur2015). The goal of the FOCLASA workshop
is to put together researchers and practitioners to share and identify
common problems, and to devise general solutions in the context of
coordination languages and self-adaptive systems.

== IMPORTANT DATES ==

17 June 2015: Deadline for abstract submission
19 June 2015: Deadline for paper submission
20 July 2015: Notifications
3 August 2015: Final versions
5 September 2015: Workshop in Madrid

== TOPICS OF INTEREST ==

(Continue reading)

S B Cooper | 18 Mar 15:48 2015
Picon

Computability in Europe 2015: Call for Informal Presentations

-------------------------------------------------------------------
  COMPUTABILITY IN EUROPE 2015: Evolving Computability
                    Bucharest, Romania
                      June 29 - July 3
               http://fmi.unibuc.ro/CiE2015/
-------------------------------------------------------------------

FUNDING DEADLINE APPROACHING 
 - ASL STUDENT TRAVEL GRANTS:  March 28, 2015

SUBMISSION DEADLINE FOR INFORMAL PRESENTATIONS:  APRIL 24, 2015
-------------------------------------------------------------------

CALL FOR INFORMAL PRESENTATIONS

There is a remarkable difference in conference style between computer 
science and mathematics conferences. Mathematics conferences allow 
for informal presentations that are prepared very shortly before the 
conference and inform the participants about current research and 
work in progress. The format of computer science conferences with 
pre-conference proceedings is not able to accommodate this form of 
scientific communication.

Continuing the tradition of past CiE conferences, also this year's 
CiE conference endeavours to get the best of both worlds. In addition 
to the formal presentations based on our LNCS proceedings volume, we 
invite researchers to present informal presentations. For this, please 
send us a brief description of your talk (between one paragraph and 
one page) by:

(Continue reading)

Michael Winter | 16 Mar 14:08 2015
Picon

CALL FOR PhD/MSc Contributions (RAMiCS 2015)

                 
Dear hol-info <at> lists.sourceforge.net,

Please find attached the final Call for Papers for RAMiCS 15 including 
extended deadlines.

Best regards

Michael Winter 
(on behalf of the organising committee)

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

                           4th CALL FOR PAPERS

                        (with deadline extension)

                 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

Scope
-----

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 disciplines.
(Continue reading)

Petros Papapanagiotou | 18 Mar 17:10 2015
Picon
Picon

Bindings for embedded languages in HOL

Hello everyone,

Having reached the ceiling of what I can achieve by "hacking" variable 
bindings and substitutions for embedded languages in HOL Light, I am now 
looking for a better way to deal with these.

I have gone through some of the results of the (now almost 10yo!) 
POPLmark challenge and subsequent papers, and I am aware of the existing 
HOAS and Nominal libraries in Coq and/or Isabelle. Has anything related 
been done in HOL Light or HOL4?

I came across the HOL4/examples/lambda theories. These may be just 
enough for what I need, but any pointers to other work that I have 
missed would be valuable.

Thank you.

Regards,
Petros

--

-- 
Petros Papapanagiotou, Ph.D.
CISA, School of Informatics
The University of Edinburgh

Email: pe.p <at> ed.ac.uk

---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
(Continue reading)

alexander.perucci | 17 Mar 17:26 2015
Picon

Projects Showcase at STAF'15 - Call for Paper

********** Projects Showcase at STAF'15 - Call for Paper **********

--- Goals and Scope
During the last decade a number of national and international financial instruments have been funding
research, innovation and development programmes. From local to global scales, many projects have been
funded delivering research and industrial innovation through reinforcing the excellence of science,
speeding up the industrial leadership, and supporting the growth of new markets. These initiatives have
been driving economic growth and creating employment opportunities, by addressing societal
challenges, boosting productivity and securing competitiveness. 

The Projects Showcase event at STAF'15 (http://www.disim.univaq.it/staf2015/projects-showcase/)
is dedicated to national and international projects dissemination and cooperation. The event provides
the opportunity for researchers and practitioners (from both academia and industry) involved in
completed, to be started or ongoing research projects related to Software Technologies - Applications
and Foundations, and hence to the topics of the leading conferences federated by STAF'15 and other
co-located events.

The Projects Showcase welcomes contributions disseminating the objectives of the project, outcomes of
specific deliverables, the final outcome of the project, as well as, advances beyond the state of the art,
overall innovation potential, exploitation approach and (expected) impact, marketing value,
barriers and obstacles. Thus, the Projects Showcase at STAF'15 represents a concrete opportunities for
participants to share experience, ideas, on-going work, and knowledge that can lead to fruitful
collaborations and cross-sectoral concertations among projects.

--- Paper Organization
Each submission should follow the following structure and clearly indicate:

- name and acronym of the project;
- source and amount of funding as well as overall total budget (if possible);
- consortium of the project or involved people;
(Continue reading)

alexander.perucci | 17 Mar 17:06 2015
Picon

SCFI 2015 Call for Papers (at IEEE SERVICES 2015)

======= SCFI 2015 Call for Papers (at IEEE SERVICES 2015) =======

IEEE Service 2015 Visionary Track on Service Composition for the Future Internet (SCFI 2015) Theme

SCFI 2015 (http://scfi2015.disim.univaq.it/) visionary track theme aims at providing innovative
contributions to the research and development of novel Service Composition approaches to assist the
design, development, validation and execution of service-oriented applications for the Future Internet.

SCFI 2014 constitutes a forum for scientists and engineers in academia and industry to present and discuss
their latest ongoing research as well as radical new research directions that represent challenging
innovations, which can advance the status quo of Service Composition when projected to the Future
Internet. 

Details on key aims of the visionary track can be found at: http://scfi2015.disim.univaq.it.

At SCFI 2015 we will have a Keynote by Paola Inverardi (Tile and abstract to be announced) - http://scfi2015.disim.univaq.it/?page_id=130

== IMPORTANT DATES ==

Submission Due Date (for all Paper types): April 19, 2015
Decision Notification on papers (Electronic): May 04, 2015
Camera-Ready Copy: May 10, 2015 

== PAPER SUBMISSION ==

All accepted papers will be included in the Proceedings of the IEEE 11th World Congress on Services
(SERVICES 2015), which will be published by the IEEE Computer Society. 

Selected papers will be invited for extension and inclusion in a special issue of a related journal.

(Continue reading)

Toby Murray | 14 Mar 02:56 2015
Picon

CFP: Programming Languages and Analysis for Security (PLAS 2015)

---------------------------------------------------------------------
Call for Papers

ACM SIGPLAN Tenth Workshop on Programming Languages and Analysis for
Security (PLAS 2015)

Prague, Czech Republic
July 2015

http://www.cs.cornell.edu/conferences/plas2015/

Co-located with ECOOP 2015 (http://2015.ecoop.org/)
---------------------------------------------------------------------

Important dates

13 April 2015 (anywhere on earth): Submissions due (no extensions)
11 May 2015: Author notification
5 June 2015: Camera-ready due
6 or 7 July 2015: Workshop (The date will be assigned by the ECOOP
organizers.)

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

PLAS aims to provide a forum for exploring and evaluating ideas on the
use of programming language and program analysis techniques to improve
the security of software systems. Strongly encouraged are proposals of
new, speculative ideas, evaluations of new or known techniques in
practical settings, and discussions of emerging threats and important
problems.  The scope of PLAS includes, but is not limited to:
(Continue reading)

Konrad Slind | 13 Mar 19:41 2015
Picon

request for literature pointers

I made the following claim in a document:

  "user errors in formally modelling artifacts and expressing properties are
   far more common than errors in the design and implementation
   of formal methods tools"

To me this seems uncontroversial, but it would be nice to be able to point
to a paper that backs this up. Off the top of my head, I can't think of any.
Can anybody help?

Thanks,
Konrad.

------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the 
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Mario Carneiro | 13 Mar 01:07 2015
Picon

Viewing HOL proofs

Hello all,

What is the usual method for "viewing" a proof stored in HOL Light, if you wanted to read it like a regular math textbook (assuming you can get over syntax difficulties)? (Of course it is not really feasible to look at the code in isolation, because you can't see the formulas.) The method I have been using so far is to copy the tactics one at a time into a HOL session using g() and e(), but it's very tedious and time-consuming, and it is also difficult to undo if you make a copying mistake during the process. (I should note that I am still a relative newbie to using HOL Light and this is essentially the only thing I have tried to do with it - I have yet to write an actual proof of my own in HOL Light.)

I feel like this is a common enough goal that there should be some program to do what I am doing and log the output. Better yet, if there was a website or downloadable collection of these proofs processed into a form that did not require interactivity in the OCaml session, this would make it much easier for mathematicians who do not necessarily want to write proofs but want to examine the many existing HOL Light proofs in order to understand them (like me). Does such a thing exist?

Mario Carneiro
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the 
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Piotr Trojanek | 13 Mar 00:39 2015
Picon

Isabelle-like "advanced rule induction" in HOL4?

Dear HOL4 experts,

Isabelle documentation ("Programming and Proving in Isabelle/HOL",
section 4.4.6) shows how one can apply "advanced rule induction" to
goals where an argument of some inductive predicate is not a variable,
for example,

"EVEN (SUC n) ==> ~ EVEN n".

I could not find anything similar in HOL4 -- did I missed something?

--

-- 
Regards,
Piotr Trojanek

------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the 
conversation now. http://goparallel.sourceforge.net/

Gmane