You can subscribe to this list here.
2003 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(12) 
_{Sep}
(8) 
_{Oct}
(20) 
_{Nov}
(21) 
_{Dec}
(3) 

2004 
_{Jan}
(16) 
_{Feb}
(11) 
_{Mar}
(26) 
_{Apr}
(15) 
_{May}
(17) 
_{Jun}
(10) 
_{Jul}
(3) 
_{Aug}
(4) 
_{Sep}
(11) 
_{Oct}

_{Nov}
(11) 
_{Dec}
(8) 
2005 
_{Jan}
(16) 
_{Feb}
(18) 
_{Mar}
(22) 
_{Apr}
(23) 
_{May}
(17) 
_{Jun}
(22) 
_{Jul}
(10) 
_{Aug}
(9) 
_{Sep}
(13) 
_{Oct}
(26) 
_{Nov}
(26) 
_{Dec}
(31) 
2006 
_{Jan}
(29) 
_{Feb}
(35) 
_{Mar}
(20) 
_{Apr}
(23) 
_{May}
(35) 
_{Jun}
(17) 
_{Jul}
(18) 
_{Aug}
(11) 
_{Sep}
(18) 
_{Oct}
(12) 
_{Nov}
(16) 
_{Dec}
(27) 
2007 
_{Jan}
(27) 
_{Feb}
(22) 
_{Mar}
(15) 
_{Apr}
(38) 
_{May}
(26) 
_{Jun}
(24) 
_{Jul}
(8) 
_{Aug}
(20) 
_{Sep}
(21) 
_{Oct}
(23) 
_{Nov}
(20) 
_{Dec}
(24) 
2008 
_{Jan}
(16) 
_{Feb}
(19) 
_{Mar}
(24) 
_{Apr}
(54) 
_{May}
(24) 
_{Jun}
(21) 
_{Jul}
(20) 
_{Aug}
(12) 
_{Sep}
(19) 
_{Oct}
(28) 
_{Nov}
(26) 
_{Dec}
(34) 
2009 
_{Jan}
(22) 
_{Feb}
(15) 
_{Mar}
(20) 
_{Apr}
(33) 
_{May}
(27) 
_{Jun}
(30) 
_{Jul}
(23) 
_{Aug}
(13) 
_{Sep}
(21) 
_{Oct}
(19) 
_{Nov}
(29) 
_{Dec}
(22) 
2010 
_{Jan}
(36) 
_{Feb}
(30) 
_{Mar}
(58) 
_{Apr}
(38) 
_{May}
(34) 
_{Jun}
(35) 
_{Jul}
(22) 
_{Aug}
(8) 
_{Sep}
(40) 
_{Oct}
(27) 
_{Nov}
(29) 
_{Dec}
(23) 
2011 
_{Jan}
(31) 
_{Feb}
(39) 
_{Mar}
(30) 
_{Apr}
(49) 
_{May}
(38) 
_{Jun}
(27) 
_{Jul}
(11) 
_{Aug}
(13) 
_{Sep}
(20) 
_{Oct}
(28) 
_{Nov}
(23) 
_{Dec}
(18) 
2012 
_{Jan}
(36) 
_{Feb}
(39) 
_{Mar}
(61) 
_{Apr}
(71) 
_{May}
(188) 
_{Jun}
(117) 
_{Jul}
(132) 
_{Aug}
(153) 
_{Sep}
(32) 
_{Oct}
(44) 
_{Nov}
(64) 
_{Dec}
(56) 
2013 
_{Jan}
(85) 
_{Feb}
(36) 
_{Mar}
(44) 
_{Apr}
(130) 
_{May}
(47) 
_{Jun}
(33) 
_{Jul}
(34) 
_{Aug}
(25) 
_{Sep}
(20) 
_{Oct}
(49) 
_{Nov}
(20) 
_{Dec}
(39) 
2014 
_{Jan}
(38) 
_{Feb}
(61) 
_{Mar}
(83) 
_{Apr}
(56) 
_{May}
(42) 
_{Jun}
(37) 
_{Jul}
(24) 
_{Aug}
(16) 
_{Sep}
(28) 
_{Oct}
(33) 
_{Nov}
(21) 
_{Dec}
(22) 
2015 
_{Jan}
(12) 
_{Feb}
(43) 
_{Mar}
(46) 
_{Apr}
(36) 
_{May}
(56) 
_{Jun}
(3) 
_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 





1
(2) 
2

3

4

5

6

7

8

9
(1) 
10

11

12

13

14

15

16
(1) 
17
(1) 
18

19
(2) 
20
(2) 
21

22

23
(1) 
24

25

26

27
(1) 
28
(3) 
29

30
(1) 
31

From: Simon Colton <sgc@do...>  20070330 19:14:18

[Apologies for crossposting] Automated Reasoning Workshop 19th  20th April 2007 Department of Computing, Imperial College, London http://www.doc.ic.ac.uk/crg/events/ARW07  CALL FOR PARTICIPATION  The 2007 automated reasoning workshop is the latest in a long series of successful workshops which aim to provide an informal forum for the automated reasoning community to discuss recent work, new ideas and current trends. It aims to bring together researchers from all areas of automated reasoning in order to foster links and facilitate crossfertilisation of ideas among researchers from various disciplines; among researchers from academia, industry and government; and between theoreticians and practitioners. Please find below details of this year's workshop:  INVITED TALKS  Geoff Sutcliffe, University of Miami Alice Miller, University of Glasgow Abstract for Geoff's talk: This talk describes the design, implementation, and testing of a system for selecting necessary axioms from a large set also containing superfluous axioms, to obtain a proof of a conjecture. The selection is determined by semantics of the axioms and conjecture, ordered heuristically by a syntactic relevance measure. The system is able to solve many problems that cannot be solved alone by the underlying automated reasoning system. Abstract for Alice's talk: Model checking is an established technique for checking the reliability of softwarecontrolled systems and constitutes one of the leading applications of logic to Computer Science. This automatic technique involves the construction of a model of a system over which properties are checked. One of the major problems with model checking is the (socalled) statespace explosion problem  where models become too large to feasibly check. A popular technique for combatting statespace explosion is symmetry reduction. In this talk I introduce a variety of model checkers and give an introduction to symmetry reduction methods, and their implementations.  EXTENDED ABSTRACTS WHICH WILL BE PRESENTED  We have a very broad and interesting selection of extended abstracts which will be presented this year. Each extended abstract will be discussed both with a short presentation and in a poster session. Forms of factoring in paramodulationbased calculi Vladimir Aleksic Compressing propositional refutations using subsumption Hasan Amjad Proof tool integration with proof general David Asipinall and Christoph Luth Towards automated verification of grid component model Alessandra Basso and Alexander Bolotov The LEOII Project Christoph Benzmuller, Larry Paulson, Frank Theiss and Arnaud Fietzke Automating Natural Deduction for Temporal Logic Alexander Bolotov, Oleg Grigoriev and Vasilyi Shangin A tableau compiled labelled deductive system for hybrid logic Krysia Broda and Alessandra Russo Towards a theory of ontology repair (or truthfulness considered harmful) Alan Bundy A rational reconstruction of a system for experimental mathematics Jacques Carette, William Farmer and Volker Sorge Cleanly combining specialised program analysers Nathaniel Charlton and Michael Huth Prediction using machine learned constraint satisfaction programs John Charnley and Simon Colton The Language EC+ Robert Craven and Marek Sergot A common semantic basis for BDI languages Louise Dennis, Rafael Bordini, Michael Fisher and Berndt Farwer Tractable temporal reasoning Clare Dixon, Michael Fisher and Boris Konev A digital library based on Mizar Jeremy Gow and Paul Cairns Proof critics for IsaPlanner Moa Johansson, Lucas Dixon and Alan Bundy Interaction and depth against nondeterminism in proof search Ozan Kahramanogullari Formal verification of implementability of timing requirements Mark Lawford, Xiayong Hu and Alan Wassung Dynamic backtracking for modal logics Zhen Li and Renate Schmidt Extensions of the KnuthBendix ordering with LPOlike properties Michel Ludwig Supporting proof in a reactive development environment Farhad Mehta Encodings of bounded LTL model checking in effectively propositional logic Juan NavarroPerez and Andrei Voronkov Using resolution to generate natural proofs David Robinson Analysis of blocking mechanisms for description logics Renate Schmidt and Dmitry Tishkovsky A universal GUI for theorem provers Bosko Stankovic, Nenad Krdzavac and Vladan Devedzic SRASS  a semantic relevance axiom selection system Geoff Sutcliffe Proving producibility of concepts Pedro Torres and Simon Colton Implementing tractable temporal logics Lan Zhang, Clare Dixon and Ulrich Hustadt  PLEASE COME ALONG TO THE WORKSHOP  Registration for the workshop has recently been opened. For details of how to register, please see the workshop web page here: http://www.doc.ic.ac.uk/crg/events/ARW07  CONTACT DETAILS  If you have any questions about the workshop, please do not hesitate to contact the workshop organiser: Simon Colton (sgc@...). 
From: Ralf Treinen <treinen@ls...>  20070328 12:04:53

SecReT 2007 2nd International Workshop on Security and Rewriting Techniques http://www.rdp07.org/secret.html June 29, 2007 Paris, France A satellite event of RDP 2007 ====================================================================== TOPICS OF INTEREST The aim of this workshop is to bring together rewriting researchers and security experts, in order to foster their interaction and develop future collaborations in this area, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. The workshop focuses on the use of rewriting techniques in all aspects of security. Specific topics include: authentication, encryption, access control and authorization, protocol verification, specification of policies, intrusion detection, integrity of information, control of information leakage, control of distributed and mobile code, etc. IMPORTANT DATES * Submissions: Monday, April 23 * Notification: Monday, May 21 * Final version due: Friday, June 8 SUBMISSION GUIDELINES Authors are invited to submit a paper (max. 10 pages) in PDF or PostScript format by April 23, 2007. Submissions should be sent by email to Monica Nesi <monica at di dot univaq dot it>. Preliminary proceedings will be available at the workshop. After the workshop authors will be invited to submit a full paper of their presentation. We plan to publish the accepted contributions in DMTCS. INVITED SPEAKER * Thomas Genet (Rennes, France) PROGRAM COMMITTEE * Véronique Cortier (Nancy, France) * Maribel Fernández (London, UK) * Paliath Narendran (Albany, NY, USA) * Monica Nesi (L'Aquila, Italy), cochair * Tobias Nipkow (München, Germany) * Hitoshi Ohsaki (Osaka, Japan) * Graham Steel (Edinburgh, UK) * MarkOliver Stehr (Stanford, CA, USA) * Ralf Treinen (Cachan, France), cochair * Luca Viganò (Verona, Italy) 
From: Jeremy Dawson <Jeremy.D<awson@rs...>  20070328 02:54:46

Xiaolei Cui wrote: > Hi all, > I am new to theorem provers. I am asked to prove that two simple > programs are equivalent(semantically), using HOL: > x:=e; if b(x) then S else T > = > if b(e) then (x:=e; S) else (x:=e; T) > > Although i have read some literatures on HOL, i still can not see the > picture here. Have anyone ever come across this kind of proof ? Any > suggestion is appreciated. > thanks a lot. > > tony Dear Tony, You need to set up a logic of programs, in HOL, as a first step. For example, you can treat the machine state as a function from variabel names to values, and then x := e is an operation that changes that state in that it changes the value of the function on the argument x. And e means e, evaluated in the state before that change of state. Then ; is composition of successive changes of state. You need to consider issues like: is the calculation of b(x) allowed to have sideeffects (change the machine state). Some of the issues are discussed in Gordon, Michael J. C., Mechanizing Programming Logics in Higher Order Logic. In G. Birtwistle and P. A. Subrahmanyam (editors), Current Trends in Hardware Verification and Automated Theorem Proving, SpringerVerlag, 1989. Also see Harrison, TPHOLs 1998, Formalising Dijkstra, pg 171188 (LNCS 1479). Also see my paper in CATS (ENTCS vol 91), Formalising General Correctness, mostly about modelling nondeterminism and nontermination together, but the first few pages may be of interest Regards, Jeremy Dawson 
From: John Harrison <John.H<arrison@cl...>  20070328 02:49:17

Hi Tony,  I am new to theorem provers. I am asked to prove that two simple  programs are equivalent(semantically), using HOL:  x:=e; if b(x) then S else T  =  if b(e) then (x:=e; S) else (x:=e; T) This shouldn't be too hard, but it depends on exactly how you formalize the programming language. For example, you can formalize a program statement like "x:=e" as a relation between possible initial and final states, as a weakest precondition a la Dijkstra, or in various other ways. Are you expected to use any specific embedding? Several people have already written programming language embeddings, or you could do it from scratch; it's not too hard. For example, sections 16 and 17 of the HOL Light tutorial http://www.cl.cam.ac.uk/~jrh13/hollight/tutorial.pdf demonstrate the formalization of a very simple language in socalled "deep" and "shallow" styles. John. 
From: Xiaolei Cui <cuix@mc...>  20070327 23:33:03

Hi all, I am new to theorem provers. I am asked to prove that two simple programs are equivalent(semantically), using HOL: x:=e; if b(x) then S else T = if b(e) then (x:=e; S) else (x:=e; T) Although i have read some literatures on HOL, i still can not see the picture here. Have anyone ever come across this kind of proof ? Any suggestion is appreciated. thanks a lot. tony 
From: Claudio Russo <crusso@mi...>  20070323 17:12:09

Below is the CFP for the 2007 Workshop on ML. As heavy users of Standard ML, we would like to invite HOL developers and users to contribute papers. Note that this year, we are introducing a new paper category of "workinprogress reports". These are intended as a way of informing others in the ML community about the status of MLrelated research or implementation projects, as well as communicating insights gained from such projects that do not quite constitute a full research paper. See the below for more details. If you are interested in submitting a paper, but you are not sure about what category it belongs in or if it would be appropriate for the workshop, please contact me or Derek Dreyer, the Programme Chair. Claudio Russo (Workshop Organizer)  The 2007 ACM SIGPLAN Workshop on ML Friday, October 5, 2007 Freiburg, Germany To be held in conjunction with ICFP '07 http://research.microsoft.com/~crusso/ml2007/ CALL FOR PAPERS GOALS OF THE WORKSHOP: The ML family of programming languages, whose most popular dialects are Standard ML and Objective Caml, has inspired a tremendous amount of computer science research, both practical and theoretical. ML continues to be employed successfully in applications ranging from compilers and theorem provers to lowlevel systems software, web applications and video games. The Workshop on ML aims to bring together researchers, developers and users of ML to hear about and discuss the latest work on the design, semantics, implementation and application of ML and MLlike languages. Previous ML workshops have been held in Orlando, Florida (1994), Baltimore, Maryland (1998), Tallinn, Estonia (2005), and Portland, Oregon (2006). The 2007 Workshop on ML will be held in conjunction with the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP 2007) in Freiburg, Germany on Friday, October 5, 2007. SUBMISSION GUIDELINES: This year, we are seeking paper submissions of two varieties: *research papers* and *workinprogress reports*. *Research papers* must present original research that has not been published elsewhere. We welcome research papers on any MLrelated topic, including (but not limited to): * applications * concurrent programming * formal semantics * language design * language formalization and mechanization * language implementation * programming environments * type systems *Workinprogress reports* need not present original research. Rather, they are intended as a way of informing others in the ML community about the status of MLrelated research or implementation projects, as well as communicating insights gained from such projects that do not quite constitute a full research paper. As such, we expect that workin progress reports will be shorter than research papers, and we will not judge them to the same standard. If you have any questions regarding the appropriate paper category for a potential submission or its overall suitability for the workshop, please contact the program chair. All paper submissions must be at most 12 pages total length in the standard ACM SIGPLAN twocolumn conference format. Authors of workinprogress report submissions should designate their papers as such by including the words "work in progress" or "status report" in the title. Submissions authored by program committee members are permitted, with the usual stipulation that they will be judged to a higher standard. Accepted papers will be published by the ACM and will appear in the ACM Digital Library. Details of the submission process will be provided at a time closer to the submission deadline. IMPORTANT DATES: Submission deadline: Friday, June 15, 2007 Notification of acceptance: Friday, July 13, 2007 Final revision due: Friday, August 3, 2007 Workshop: Friday, October 5, 2007 WORKSHOP ORGANIZER: * Claudio Russo (Microsoft Research, Cambridge) PROGRAM CHAIR: * Derek Dreyer (Toyota Technological Institute at Chicago) PROGRAM COMMITTEE: * Lars Birkedal (IT University of Copenhagen) * Derek Dreyer (Toyota Technological Institute at Chicago) * Jacques Garrigue (Nagoya University) * Luc Maranget (INRIA Rocquencourt) * Greg Morrisett (Harvard University) * Atsushi Ohori (Tohoku University) * Peter Sestoft (IT University of Copenhagen) * Peter Sewell (University of Cambridge) * Mark Shinwell (CodeSourcery UK Ltd) * Don Syme (Microsoft Research, Cambridge) 
From: Freek Wiedijk <freek@cs...>  20070320 19:35:06

Programming Languages for Mechanized Mathematics Workshop As part of Calculemus 2007 <http://www.risc.unilinz.ac.at/about/conferences/Calculemus2007/>; Hagenberg, Austria [http://www.cas.mcmaster.ca/plmms07/] The intent of this workshop is to examine more closely the intersection between programming languages and mechanized mathematics systems (MMS). By MMS, we understand computer algebra systems (CAS), [automated] theorem provers (TP/ATP), all heading towards the development of fully unified systems (the MMS), sometimes also called universal mathematical assistant systems (MAS) (see Calculemus 2007 <http://www.risc.unilinz.ac.at/about/conferences/Calculemus2007/>;). There are various ways in which these two subjects of /programming languages/ and /systems for mathematics/ meet: * Many systems for mathematics contain a dedicated programming language. For instance, most computer algebra systems contain a dedicated language (and are frequently built in that same language); some proof assistants (like the Ltac language for Coq) also have an embedded programming language. Note that in many instances this language captures only algorithmic content, and /declarative/ or /representational/ issues are avoided. * The /mathematical languages/ of many systems for mathematics are very close to a functional programming language. For instance the language of ACL2 is just Lisp, and the language of Coq is very close to Haskell. But even the mathematical language of the HOL system can be used as a functional programming language that is very close to ML and Haskell. On the other hand, these languages also contain very rich specification capabilities, which are rarely available in most computationoriented programming languages. And even then, many specification languages ((B, Z, Maude, OBJ3, CASL, etc) can still teach MMSes a trick or two regarding representational power. * Conversely, functional programming languages have been getting "more mathematical" all the time. For instance, they seem to have discovered the value of dependent types rather recently. But they are still not quite ready to 'host' mathematics (the nonsuccess of docon <http://www.haskell.org/docon/>; being typical). There are some promising languages on the horizon (Epigram <http://www.epig.org/>;, Omega <http://web.cecs.pdx.edu/%7Esheard/Omega/index.html>;) as well as some hybrid systems (Agda <http://agda.sourceforge.net/>;, Focal <http://focal.inria.fr/site/index.php>;), although it is unclear if they are truly capable of expressing the full range of ideas present in mathematics. * Systems for mathematics are used to prove programs correct. (One method is to generate "correctness conditions" from a program that has been annotated in the style of Hoare logic and then prove those conditions in a proof assistant.) An interesting question is what improvements are needed for this both on the side of the mathematical systems and on the side of the programming languages. We are interested in all these issues. We hope that a certain synergy will develop between those issues by having them explored in parallel. These issues have a very colourful history. Many programming language innovations first appeared in either CASes or Proof Assistants, before migrating towards more mainstream languages. One can cite (in no particular order) type inference, dependent types, generics, termrewriting, firstclass types, firstclass expressions, firstclass modules, code extraction, and so on. However, a number of these innovations were never aggressively pursued by system builders, letting them instead be developped (slowly) by programming language researchers. Some, like type inference and generics have flourished. Others, like firstclass types and firstclass expressions, are not seemingly being researched by anyone. We want to critically examine what has worked, and what has not. Why are all the current ``popular'' computer algebra systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? But also look at question like what forms of polymorphism exists in mathematics? What forms of dependent types exist in mathematics? How can MMS regain the upper hand on issues of 'genericity'? What are the biggest barriers to using a more mainstream language as a host language for a CAS or an ATP? This workshop will accept two kinds of submissions: full research papers as well as position papers. Research papers should be nore more than 15 pages in length, and positions papers no more than 3 pages. Submission will be through _EasyChair_. An informal version of the proceedings will be available at the workshop, with a more formal version to appear later. We are looking into having the best papers completed into full papers and published as a special issue of a Journal (details to follow). Important Dates April 25, 2007: Submission Deadline June 2930, 2007: Workshop Program Committee Lennart Augustsson <http://www.cs.chalmers.se/%7Eaugustss>; [Credit Suisse] Wieb Bosma <http://www.math.ru.nl/%7Ebosma/>[Radboud University Nijmegen, Netherlands] Jacques Carette <http://www.cas.mcmaster.ca/%7Ecarette>; (coChair) [McMaster University, Canada] David Delahaye <http://cedric.cnam.fr/%7Edelahaye/>; [CNAM, France] JeanChristophe Filliâtre <http://www.lri.fr/%7Efilliatr/>; [CNRS and Université de ParisSud, France] John Harrison <http://www.cl.cam.ac.uk/%7Ejrh13/>; [Intel Corporation, USA] Markus (Makarius) Wenzel <http://www4.in.tum.de/%7Ewenzelm/>; [Technische Universität München, Germany] Freek Wiedijk <http://www.cs.ru.nl/%7Efreek/>; (coChair) [Radboud University Nijmegen, Netherlands] Wolfgang Windsteiger <http://www.risc.unilinz.ac.at/people/wwindste/>; [University of Linz, Austria] Location and Registration Location and registration information can be found on the Calculemus <http://www.risc.unilinz.ac.at/about/conferences/Calculemus2007/>; web site. 
From: TPHOLs 2007 Organisers <tphols2007@in...>  20070320 12:15:50

HTMLversion of the results table: http://rsg.informatik.unikl.de/TPHOLs2007/tphols2008.html Election Result 1st choice 2nd choice 3rd choice 1st round 2nd round 3rd round Hagenberg Montreal Sydney 1 Hagenberg Montreal  2 Hagenberg   1 Hagenberg Sydney  0 Hagenberg Sydney Montreal 2 Montreal Hagenberg Sydney 8 Montreal Hagenberg  5 Montreal   10 17 49 Montreal Sydney  1 14 Montreal Sydney Hagenberg 4 Sydney Hagenberg Montreal 5 Sydney Hagenberg  2 Sydney   10 12 Sydney Montreal  4 18 Sydney Montreal Hagenberg 7    0 1 13 total 62 62 62 The TPHOLs 2007 Organizing Committee are therefore pleased to announce that TPHOLs 2008 will be held at Concordia University, Montreal, organised by Sofiene Tahr. Thank you to everyone who participated in the selection process, and especially Martin, Sofiene and Alessandro for proposing bids. Jens 
From: <sawada@us...>  20070319 17:45:53

ACL2 2007 International Workshop on the ACL2 Theorem Prover and its Applications http://www.cs.uwyo.edu/~ruben/acl207 CALL FOR PAPERS November 1516, 2007 in Austin, Texas Hosted by FMCAD 2007 IMPORTANT DATES Abstract submission: July 2, 2007 Paper submission: July 9, 2007 Acceptance Notification: September 3, 2007 Final Version Due: October 15, 2007 CONFERENCE SCOPE ACL2 2007 is the major technical forum for users of the ACL2 theorem proving system and is the seventh in a series of workshops that occur approximately every 18 months. ACL2 is an industrialstrength automated reasoning system that is part of the BoyerMoore family of theorem provers, for which its authors received the 2005 ACM Software System Award. ACL2 2007 is hosted by FMCAD. We invite papers on any topics related to ACL2, and we encourage submission of papers related to other theorem provers or formal methods that can be contributed to the ACL2 community. Suggested topics include but are not limited by the following: * software or hardware verification with the theorem prover, * formalizations of mathematics in ACL2, * new libraries, tools, and interfaces for ACL2, * experiences with ACL2 in the classroom, * reports of and proposals for improvements of ACL2, * comparisons with other theorem provers * comparisons with other programming or specification languages, * challenge problems and their solutions, * foundational issues related to ACL2, and * implementations connecting ACL2 with other systems. PAPER SUBMISSIONS Submissions must be made electronically in PDF format, as directed in the ACL2 2007 website. Submissions should be prepared in the ACM SIG Proceeding Templates, available from http://www.acm.org/sigs/pubs/proceed/template.html. We strongly prefer submissions in the "LaTeX2e  Strict Adherence to the SIGS Style". The ACL2 Workshop accepts both long papers (up to ten pages) and short papers (up to four pages). Both categories of papers will be fully refereed. At least one author of each accepted papers must register for the workshop and give a presentation summarizing the paper's results. Authors of long papers will have more time to present their work at the workshop; this is the primary distinction between long and short papers. One of the main advantages of the ACL2 Workshop is that attendees are already knowledgeable about ACL2, its syntax, its basic commands, and the art of writing models in it. So authors may assume that readers have this familiarity. We expect to provide workshop proceedings and to include these proceedings in the ACM digital library. Many papers presented at the workshop will describe interactions with the theorem prover. We strongly encourage authors of such papers to provide ACL2 script files (aka "books") along with instructions for using these books in ACL2. Such supporting materials should follow the guidelines at http://www.cs.utexas.edu/users/moore/acl2/books/index.html. For accepted papers, these books will be mirrored on the ACL2 home page and included in future ACL2 distributions. ORGANIZATION Chairs * Ruben Gamboa, University of Wyoming * Jun Sawada, IBM Austin Research Laboratory * John Cowles, University of Wyoming Program Committee * David Greve, Rockwell Collins, Inc. * John Harrison, Intel Corporation * Warren Hunt, University of Texas * Deepak Kapur, University of New Mexico * Matt Kaufmann, University of Texas * Bill Legato, NSA * Mike Lowry, NASA * Panagiotis Manolios, Georgia Institute of Technology * John Mathews, Galois Connections * Jose Meseguer, University of Illinois * Paul Miner, NASA * J Strother Moore, University of Texas * Rex Page, University of Oklahoma * Jose Luis RuizReina, University of Seville * Laurence Pierre, Université de Nice SophiaAntipolis, Laboratoire TIMA * David Russinoff, Advanced Micro Devices, Inc. * Konrad Slind, University of Utah * Matt Wilding, Rockwell Collins, Inc. 
From: TPHOLs 2007 Organisers <tphols2007@in...>  20070319 09:00:32

HTMLversion of the results table: http://rsg.informatik.unikl.de/TPHOLs2007/tphols2008.html Election Result 1st choice 2nd choice 3rd choice 1st round 2nd round 3rd round Hagenberg Montreal Sydney 1 Hagenberg Montreal  2 Hagenberg   1 Hagenberg Sydney  0 Hagenberg Sydney Montreal 2 Montreal Hagenberg Sydney 8 Montreal Hagenberg  5 Montreal   10 17 49 Montreal Sydney  1 14 Montreal Sydney Hagenberg 4 Sydney Hagenberg Montreal 5 Sydney Hagenberg  2 Sydney   10 12 Sydney Montreal  4 18 Sydney Montreal Hagenberg 7    0 1 13 total 62 62 62 The TPHOLs 2007 Organizing Committee are therefore pleased to announce that TPHOLs 2008 will be held at Concordia University, Montreal, organised by Sofiene Tahr. Thank you to everyone who participated in the selection process, and especially Martin, Sofiene and Alessandro for proposing bids. Jens 
From: Luca Vigano <vigano@in...>  20070317 11:55:09

apologies for multiple copies ************************ **** **** **** FCSARSPA'07 **** **** **** ************************ A LICS'07 and ICALP'07 Affiliated Workshop on FOUNDATIONS OF COMPUTER SECURITY and AUTOMATED REASONING FOR SECURITY PROTOCOL ANALYSIS Wroclaw, Poland, July 89, 2007 http://profs.sci.univr.it/~vigano/fcsarspa07 *********************** *** SECOND *** *** CALL FOR PAPERS *** *********************** Submission deadline: April 15, 2007 BACKGROUND, AIM AND SCOPE ========================= Computer security is an established field of computer science of both theoretical and practical significance. In recent years, there has been increasing interest in logicbased foundations for various methods in computer security, including the formal specification, analysis and design of security protocols and their applications, the formal definition of various aspects of security such as access control mechanisms, mobile code security and denialofservice attacks, and the modeling of information flow and its application to confidentiality policies, system composition, and covert channel analysis. The workshop FCSARSPA'07 is the second edition of the fusion of two workshops: FCS and ARSPA, which joined forces in 2006 for FCSARSPA'06, which was affiliated to LICS'06, in the context of FLoC'06. The workshop FCS continues a tradition, initiated with the Workshops on Formal Methods and Security Protocols (FMSP) in 1998 and 1999, then with the Workshop on Formal Methods and Computer Security (FMCS) in 2000, and finally with the LICS satellite Workshop on Foundations of Computer Security (FCS) in 2002 through 2005, of bringing together formal methods and the security community. ARSPA is a series of workshops on Automated Reasoning for Security Protocol Analysis, bringing together researchers and practitioners from both the security and the formal methods communities, from academia and industry, who are working on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. The first two ARSPA workshops were held as satellite events of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04) and of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), respectively. The aim of the joint workshop FCSARSPA'07 is to provide a forum for continued activity in these areas, to bring computer security researchers in closer contact with the LICS and ICALP communities, and to give LICS and ICALP attendees an opportunity to talk to experts in computer security. We thus solicit submissions of papers both on mature work and on work in progress. We are interested both in new results in theories of computer security and also in more exploratory presentations that examine open questions and raise fundamental concerns about existing theories, as well as in new results on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. Possible topics include, but are not limited to: Automated reasoning techniques Access control and resource usage control Composition issues Authentication Formal specification Availability and denial of service Foundations of verification Covert channels Information flow analysis Confidentiality Languagebased security Integrity and privacy Logicbased design for Intrusion detection Program transformation Malicious code Security models Mobile code Static analysis Mutual distrust Statistical methods Privacy Tools Security policies Trust management Security protocols All submissions will be peerreviewed. Authors of accepted papers must guarantee that their paper will be presented at the workshop. SUBMISSION ========== Submissions should be at most 15 pages (a4paper, 11pt), including references, in the Springer LNCS style available at the URL http://www.springer.de/comp/lncs/authors.html The cover page should include title, names of authors, coordinates of the corresponding author, an abstract, and a list of keywords. It is recommended that submissions adhere to the specified format and length. Submissions that are clearly too long may be rejected immediately. Additional material intended for the referees but not for publication in the final version  for example details of proofs  may be placed in a clearly marked appendix that is not included in the page limit. Simultaneous submissions to a journal or another conference are accepted, unless the rules for the journal or the other conference exclude such a possibility. If the paper is accepted to both FCSARSPA'07 and the other venue, it is the responsibility of the authors to promptly notify FCSARSPA'07 chairs and to acknowledge copyright holders. Authors are invited to submit their papers electronically, as portable document format (pdf) or postscript (ps); please, do not send files formatted for work processing packages (e.g., Microsoft Word or Wordperfect files). The only mechanism for paper submissions is via the electronic submission website (which will soon be available). IMPORTANT DATES =============== Papers due: April 15, 2007 Notification of acceptance: May 20, 2007 Final paper versions due: June 10, 2007 Workshop: July 0809, 2007 PUBLICATION =========== Informal proceedings will be made available in electronic format and they will be distributed to all participants of the workshop. A journal special issue associated to the workshop (but open also to nonparticipants, in all cases with fresh reviewing) is planned. INVITED TALKS ============= To be announced PROGRAM COMMITTEE ================= * Alessandro Armando (Universita` di Genova, Italy) * Anindya Banerjee (Kansas State University, USA) * Massimo Bartoletti (Universita` di Pisa, Italy) * Michele Boreale (Universita` di Firenze, Italy) * Yannick Chevalier (IRIT Toulouse, France) * Veronique Cortier (LORIA Nancy, France) * Cas Cremers (ETH Zurich, Switzerland) * Pierpaolo Degano (Universita` di Pisa, Italy; cochair) * Ralf Kuesters (ETH Zurich, Switzerland; cochair) * Volkmar Lotz (SAP Labs France) * Cathy Meadows (Naval Research Laboratory, USA) * Sebastian Moedersheim (IBM Zurich Research Lab, Switzerland) * David Naumann (Stevens Institute of Technology, USA) * Mark Ryan (University of Birmingham, U.K.) * Eijiro Sumii (Tohoku University, Japan) * Luca Vigano` (Universita` di Verona, Italy; cochair) * Steve Zdancewic (University of Pennsylvania, USA; cochair) FCS Steering Committee: * Martin Abadi (University of California at Santa Cruz, USA) * John Mitchell (Stanford University, USA) * Andrei Sabelfeld (Chalmers, Sweden; chair) * Andre Scedrov (University of Pennsylvania, USA) * Luca Vigano` (Universita` di Verona, Italy) ADDITIONAL INFORMATION ====================== Information about registration, travel, and venue can be found on the LICS'07 website and on the ICALP'07 website. For further information send an email to the workshop cochairs at the address specified on the workshop's website. 
From: Ofer Strichman <ofers@ie...>  20070316 14:38:57

Call for Papers: Fifth International Workshop on Bounded Model Checking (BMC'07) ************************************************************************ When: July 8th, 2007 (a day after CAV'07) Where: Berlin, Germany BMC'07 is affiliated with the 19th International Conference on ComputerAided Verification (CAV'07). URL: http://ie.technion.ac.il/BMC07 contact: bmc07@... Chairs  Armin Biere, Johannes Kepler University, Linz, Austria Ofer Strichman, Technion, Haifa, Israel Important Dates  Submissions: April 22, 2007 Notification: May 21, 2007 Final Papers: June 3, 2007 Workshop: July 8, 2007 Objective Scope  The scope of the workshop includes all theoretical and practical aspects of Bounded Model Checking, including, but not limited to, using SAT technology for unbounded model checking, combining BMC with other tools and techniques, experimental results in an industrial setting, BMC of infinite state systems, translation schemes, and dedicated SAT techniques for BMC. Information about the submission process can be found in the BMC web page. 
From: Simon Colton <sgc@do...>  20070309 14:06:04

[Apologies for crossposting] ================================================================ FINAL CALL FOR PAPERS (1 week until the deadline...) 2007 Workshop on Automated Reasoning Bridging the Gap between Theory and Practice 19th20th April 2007 Department of Computing Imperial College, London http://www.doc.ic.ac.uk/crg/events/ARW07 *** 2side Extended Abstracts Due: 16th March 2007 *** ================================================================ Invited Speakers  Geoff Sutcliffe (University of Miami) http://www.cs.miami.edu/~geoff/ "SRASS  a Semantic Relevance Axiom Selection System" Alice Miller (University of Glasgow) http://www.dcs.gla.ac.uk/~alice/ "Symmetry reduction methods for model checking" ================================================================ Topics  The workshop will cover the full breadth and diversity of automated reasoning and will include topics such as: Theorem proving in classical and nonclassical logics Reasoning systems and mechanisms: Description logics Equational reasoning, unification Induction Constraint Satisfaction Combining reasoning systems Specialised decision procedures Formal methods in software analysis: Verification Nonclassical inference: Nonmonotonic reasoning, abduction Intuitionistic reasoning Logicbased knowledge representation: Ontology specification, Domain specific reasoning (spatial, temporal, epistemic etc.) Reasoning for agents (or about agents) Interactive theorem proving Implementation issues and empirical results Applications of automated reasoning ================================================================ Submissions  We invite interested persons to submit a cameraready, twopage extended abstract about recent work or work in progress, or a system description. Anyone wishing to attend but not interested in presenting should send a shorter position statement (1/2  1 page). Submissions should be sent in in either Postscript or PDF format by email to the workshop organisers at: sgc@... Please use the LaTeX style file provided on the workshop web page: http://www.doc.ic.ac.uk/crg/events/ARW07 Each submission should include the names and complete addresses (including email) of all authors. Correspondence will be sent to the first author, unless otherwise indicated. The main objective of the abstracts is to spread information about recent work in our community, and we expect to accept most intopic submissions, but we may ask for revisions. Abstracts will be published in informal workshop notes and be made available on the internet. ================================================================ Presentations  Each workshop attendee will be allocated a 5 minute slot (or a 10 minute slot, depending on time constraints), for a short talk to introduce their research. Each attendee will also be allocated space in a poster session, where they can further present and discuss their work. Please prepare posters for the event. ================================================================ Studentships  A limited number of studentships will be available to fund travel and accomodation expenses. Applications for studentships will require written proof of student status, and must be received by the deadline below. Payment is made by cheque during or after the symposium. To indicate your interest, please send a short email to Jacques Fleuriot (jdf@...) any time before 9th March 2007. ================================================================ ARW Meal  We will organise a workshop meal in a lovely restaurant in the South Kensington area. Details coming soon... ================================================================ Organisers  The workshop is being organised by the Combined Reasoning Group at Imperial College: http://www.doc.ic.ac.uk/crg ================================================================ Program Committee  Clare Dixon, Chair (University of Liverpool) Jacques Fleuriot Secretary/Treasurer (University of Edinburgh) Brandon Bennett (University of Leeds) Simon Colton (Imperial College London) David Crocker (Escher Technologies) Louise Dennis (University of Liverpool) Roy Dyckhoff (University of St Andrews) Ulle Endriss, (University of Amsterdam) Alan Frisch (University of York) Ullrich Hustadt (University of Liverpool) Mateja Jamnik (Univerity of Cambridge) Tom Melham (University of Oxford) Renate Schmidt (University of Manchester) Volker Sorge (University of Birmingham) ================================================================ Important Dates  Applications for Studentships: 9th March 2007 Submission of 2side extended abstracts: 16th March 2007 Notification of decision: 23rd March 2007 Camera ready copies required by: 30th March 2007 Automated Reasoning Workshop: 19th and 20th April 2007 ================================================================ Contact  Please email Simon Colton (sgc@...) if you have any queries about the 2007 Automated Reasoning Workshop. ================================================================ 
From: Konrad Slind <slind@cs...>  20070301 18:36:13

Hi Juan, You can define the function you want: > Define `(even 0n = T) /\ > (odd 0n = F) /\ > (even n = odd (n1)) /\ > (odd n = even (n1))`; > Equations stored under "even_def". > Induction stored under "even_ind". > > val it = >  (even 0 = T) /\ (odd 0 = F) /\ (even (SUC v2) = odd (SUC v2  > 1)) /\ > (odd (SUC v4) = even (SUC v4  1)) : thm If Define fails because its automated termination prover is not strong enough, you can use Hol_defn to define the function and prove termination manually. This is discussed in the Description document. If want to define inductive relations, use Hol_reln: > Hol_reln `even(0n) /\ odd(1n) /\ > (!n. even(n) ==> odd(n + 1)) /\ > (!n. odd(n) ==> even(n + 1))`;; > > val it = > ( even 0 /\ odd 1 /\ (!n. even n ==> odd (n + 1)) /\ > !n. odd n ==> even (n + 1), >  !odd' even'. > even' 0 /\ odd' 1 /\ (!n. even' n ==> odd' (n + 1)) /\ > (!n. odd' n ==> even' (n + 1)) ==> > (!a0. odd a0 ==> odd' a0) /\ !a1. even a1 ==> even' a1, >  (!a0. odd a0 = (a0 = 1) \/ ?n. (a0 = n + 1) /\ even n) /\ > !a1. even a1 = (a1 = 0) \/ ?n. (a1 = n + 1) /\ odd n) : thm * > thm * thm Konrad. On Mar 1, 2007, at 4:03 AM, Juan Perna wrote: > Hello, > > I am new at HOL and this will be, quite likely, a very simple question: > I am trying to create an inductive definition for a recursive function. > I have tried already with the normal 'Define' command but it fails to > prove termination automatically for the function I need. > > Then, I am trying to use `new_inductive_definition` from the > 'InductiveDefinition' theory but I can't manage to have the first "let" > in the examples working, i.e.: > > LET eo_RULES,eo_INDUCT, eo_CASES = new_inductive_definition > `even(0) /\ odd(1) /\ > (!n. even(n) ==> odd(n + 1)) /\ > (!n. odd(n) ==> even(n + 1))`;; > > I know this is an example from HOL Lite but I haven't been able to find > an example from HOL Kananaskis. > > Can anybody provide me with an example of how to use > `new_inductive_definition` to define a function/relation inductively? > > Thank you very much > > Juan > > >  >  > Take Surveys. Earn Cash. Influence the Future of IT > Join SourceForge.net's Techsay panel and you'll get the chance to > share your > opinions on IT & business topics through brief surveysand earn cash > http://www.techsay.com/default.php? > page=join.php&p=sourceforge&CID=DEVDEV > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo 
From: Juan Perna <jiperna@cs...>  20070301 11:07:59

Hello, I am new at HOL and this will be, quite likely, a very simple question: I am trying to create an inductive definition for a recursive function. I have tried already with the normal 'Define' command but it fails to prove termination automatically for the function I need. Then, I am trying to use `new_inductive_definition` from the 'InductiveDefinition' theory but I can't manage to have the first "let" in the examples working, i.e.: LET eo_RULES,eo_INDUCT, eo_CASES = new_inductive_definition `even(0) /\ odd(1) /\ (!n. even(n) ==> odd(n + 1)) /\ (!n. odd(n) ==> even(n + 1))`;; I know this is an example from HOL Lite but I haven't been able to find an example from HOL Kananaskis. Can anybody provide me with an example of how to use `new_inductive_definition` to define a function/relation inductively? Thank you very much Juan 