2003: 2004: 2005: 2006: 2007: 2008: 2009: 2010: 2011: 2012: 2013: Jan Feb Mar Apr May Jun Jul Aug (12) Sep (8) Oct (20) Nov (21) Dec (3) Jan (16) Feb (11) Mar (26) Apr (15) May (17) Jun (10) Jul (3) Aug (4) Sep (11) Oct Nov (11) Dec (8) Jan (16) Feb (18) Mar (22) Apr (23) May (17) Jun (22) Jul (10) Aug (9) Sep (13) Oct (26) Nov (26) Dec (31) Jan (29) Feb (35) Mar (20) Apr (23) May (35) Jun (17) Jul (18) Aug (11) Sep (18) Oct (12) Nov (16) Dec (27) Jan (27) Feb (22) Mar (15) Apr (38) May (26) Jun (24) Jul (8) Aug (20) Sep (21) Oct (23) Nov (20) Dec (24) Jan (16) Feb (19) Mar (24) Apr (54) May (24) Jun (21) Jul (20) Aug (12) Sep (19) Oct (28) Nov (26) Dec (34) Jan (22) Feb (15) Mar (20) Apr (33) May (27) Jun (30) Jul (23) Aug (13) Sep (21) Oct (19) Nov (29) Dec (22) Jan (36) Feb (30) Mar (58) Apr (38) May (34) Jun (35) Jul (22) Aug (8) Sep (40) Oct (27) Nov (29) Dec (23) Jan (31) Feb (39) Mar (30) Apr (49) May (38) Jun (27) Jul (11) Aug (13) Sep (20) Oct (28) Nov (23) Dec (18) Jan (36) Feb (39) Mar (61) Apr (71) May (188) Jun (117) Jul (132) Aug (153) Sep (32) Oct (44) Nov (64) Dec (56) Jan (85) Feb (36) Mar (44) Apr (130) May (47) Jun (33) Jul (34) Aug (25) Sep (20) Oct (49) Nov (20) Dec (28)
S M T W T F S
1 2 3
(2)
4 5 6 7 8 9 10
(1)
11 12 13 14 15 16 17
(1) (1)
18 19 20 21 22 23 24
(2) (2)     (1)
25 26 27 28 29 30 31
(1) (3)   (1)
 hol-builds hol-info hol-checkins hol-developers Nested Flat Threaded Ultimate Show 25 Show 50 Show 75 Show 100
 [Hol-info] Having no idea on proving equivalency between programs. Thanks From: Xiao-lei Cui - 2007-03-27 23:33 ```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 ```

 Re: [Hol-info] Having no idea on proving equivalency between programs. Thanks From: Jeremy Dawson - 2007-03-28 02:54 ```Xiao-lei 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 side-effects (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, Springer-Verlag, 1989. Also see Harrison, TPHOLs 1998, Formalising Dijkstra, pg 171-188 (LNCS 1479). Also see my paper in CATS (ENTCS vol 91), Formalising General Correctness, mostly about modelling non-determinism and non-termination together, but the first few pages may be of interest Regards, Jeremy Dawson ```

 Re: [Hol-info] Having no idea on proving equivalency between programs. Thanks From: John Harrison - 2007-03-28 02:49 ```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/hol-light/tutorial.pdf demonstrate the formalization of a very simple language in so-called "deep" and "shallow" styles. John. ```

 [Hol-info] CFP: The 2007 ACM SIGPLAN Workshop on ML (Call For Papers) From: Claudio Russo - 2007-03-23 17:12 ```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 "work-in-progress reports". These are intended as a way of informing others in the ML community about the status of ML-related 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 low-level 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 ML-like 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 *work-in-progress reports*. *Research papers* must present original research that has not been published elsewhere. We welcome research papers on any ML-related topic, including (but not limited to): * applications * concurrent programming * formal semantics * language design * language formalization and mechanization * language implementation * programming environments * type systems *Work-in-progress reports* need not present original research. Rather, they are intended as a way of informing others in the ML community about the status of ML-related 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 work-in- 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 two-column conference format. Authors of work-in-progress 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) ```

 [Hol-info] Programming Languages for Mechanized Mathematics Workshop From: Freek Wiedijk - 2007-03-20 19:35 ```Programming Languages for Mechanized Mathematics Workshop As part of Calculemus 2007 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 ). 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 computation-oriented 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 non-success of docon being typical). There are some promising languages on the horizon (Epigram , Omega ) as well as some hybrid systems (Agda , Focal ), 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, term-rewriting, first-class types, first-class expressions, first-class 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 first-class types and first-class 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 29-30, 2007: Workshop Program Committee Lennart Augustsson [Credit Suisse] Wieb Bosma [Radboud University Nijmegen, Netherlands] Jacques Carette (co-Chair) [McMaster University, Canada] David Delahaye [CNAM, France] Jean-Christophe Filliâtre [CNRS and Université de Paris-Sud, France] John Harrison [Intel Corporation, USA] Markus (Makarius) Wenzel [Technische Universität München, Germany] Freek Wiedijk (co-Chair) [Radboud University Nijmegen, Netherlands] Wolfgang Windsteiger [University of Linz, Austria] Location and Registration Location and registration information can be found on the Calculemus web site. ```

 [Hol-info] TPHOLs 2008: Election Result From: TPHOLs 2007 Organisers - 2007-03-19 09:00 ```HTML-version of the results table: http://rsg.informatik.uni-kl.de/TPHOLs-2007/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 ```

 [Hol-info] TPHOLs 2008: Election Result From: TPHOLs 2007 Organisers - 2007-03-20 12:15 ```HTML-version of the results table: http://rsg.informatik.uni-kl.de/TPHOLs-2007/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 ```

 [Hol-info] ACL2 2007 CALL FOR PAPER From: - 2007-03-19 17:45 ```ACL2 2007 International Workshop on the ACL2 Theorem Prover and its Applications http://www.cs.uwyo.edu/~ruben/acl2-07 CALL FOR PAPERS November 15-16, 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 industrial-strength automated reasoning system that is part of the Boyer-Moore 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 Ruiz-Reina, University of Seville * Laurence Pierre, Université de Nice Sophia-Antipolis, Laboratoire TIMA * David Russinoff, Advanced Micro Devices, Inc. * Konrad Slind, University of Utah * Matt Wilding, Rockwell Collins, Inc. ```

 [Hol-info] CFP: FCS-ARSPA'07 (Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis) From: Luca Vigano - 2007-03-17 11:55 ```apologies for multiple copies ************************ **** **** **** FCS-ARSPA'07 **** **** **** ************************ A LICS'07 and ICALP'07 Affiliated Workshop on FOUNDATIONS OF COMPUTER SECURITY and AUTOMATED REASONING FOR SECURITY PROTOCOL ANALYSIS Wroclaw, Poland, July 8-9, 2007 http://profs.sci.univr.it/~vigano/fcs-arspa07 *********************** *** 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 logic-based 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 denial-of-service attacks, and the modeling of information flow and its application to confidentiality policies, system composition, and covert channel analysis. The workshop FCS-ARSPA'07 is the second edition of the fusion of two workshops: FCS and ARSPA, which joined forces in 2006 for FCS-ARSPA'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 FCS-ARSPA'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 Language-based security Integrity and privacy Logic-based 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 peer-reviewed. 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, co-ordinates 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 FCS-ARSPA'07 and the other venue, it is the responsibility of the authors to promptly notify FCS-ARSPA'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 web-site (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 08-09, 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 non-participants, 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; co-chair) * Ralf Kuesters (ETH Zurich, Switzerland; co-chair) * 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; co-chair) * Steve Zdancewic (University of Pennsylvania, USA; co-chair) 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 web-site and on the ICALP'07 web-site. For further information send an email to the workshop co-chairs at the address specified on the workshop's web-site. ```

 [Hol-info] Call for papers: The 5th iworkshop on Bounded Model Checking (BMC'07) From: Ofer Strichman - 2007-03-16 14:38 ```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 Computer-Aided 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. ```

 [Hol-info] Automated Reasoning Workshop 2007 - Final CFP From: Simon Colton - 2007-03-09 14:06 ```[Apologies for cross-posting] ================================================================ FINAL CALL FOR PAPERS (1 week until the deadline...) 2007 Workshop on Automated Reasoning Bridging the Gap between Theory and Practice 19th-20th April 2007 Department of Computing Imperial College, London http://www.doc.ic.ac.uk/crg/events/ARW07 *** 2-side 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 non-classical 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 Non-classical inference: Non-monotonic reasoning, abduction Intuitionistic reasoning Logic-based 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 camera-ready, two-page 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 in-topic 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 2-side 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. ================================================================ ```

 [Hol-info] new_inductive_definition From: Juan Perna - 2007-03-01 11:07 ```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 ```

 Re: [Hol-info] new_inductive_definition From: Konrad Slind - 2007-03-01 18:36 ```Hi Juan, You can define the function you want: > Define `(even 0n = T) /\ > (odd 0n = F) /\ > (even n = odd (n-1)) /\ > (odd n = even (n-1))`; > 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 surveys-and earn cash > http://www.techsay.com/default.php? > page=join.php&p=sourceforge&CID=DEVDEV > _______________________________________________ > hol-info mailing list > hol-info@... > https://lists.sourceforge.net/lists/listinfo/hol-info ```