http://permalink.gmane.org/gmane.comp.mathematics.hol hourly 1 1901-01-01T00:00+00:00 http://gmane.org/img/gmane-25t.png http://gmane.org http://permalink.gmane.org/gmane.comp.mathematics.hol/2706 <pre>===================================================== ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13) http://complogic.cs.mcgill.ca/lfmtp13 23 September, 2013 Boston, USA Co-located with with ICFP'13 CALL FOR PAPERS ===================================================== IMPORTANT DATES Paper submission: June 14, 2013 Author notification: July 7, 2013 Final versions due: July 18, 2013 ===================================================== Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems on the other hand have been the focus of considerable res</pre> Brigitte Pientka 2013-05-22T03:06:39 http://permalink.gmane.org/gmane.comp.mathematics.hol/2705 <pre>25th OpenMath Workshop Bath, UK 10 July 2013 co-located with CICM 2013 Submission deadline 7 June http://www.cicm-conference.org/2013/openmath/ OBJECTIVES OpenMath (http://www.openmath.org) is a language for exchanging mathematical formulae across applications (such as computer algebra systems). From 2010 its importance has increased in that OpenMath Content Dictionaries were adopted as a foundation of the MathML 3 W3C recommendation (http://www.w3.org/TR/MathML), the standard for mathematical formulae on the Web. Topics we expect to see at the workshop include * Feature Requests (Standard Enhancement Proposals) and Discussions for going beyond OpenMath 2; * Further convergence of OpenMath and MathML 3; * Reasoning with OpenMath; * Software using or processing OpenMath; * OpenMath on the Semantic Web; * New OpenMath Content Dictionaries; Contributions can be either full research papers, Standard Enhancement Proposals, or a description of new Content Dictionaries, particularly on</pre> Christoph LANGE 2013-05-20T11:10:28 http://permalink.gmane.org/gmane.comp.mathematics.hol/2704 <pre>*To be removed from our mailing list, please respond to this message with UNSUBSCRIBE in the subject line* ********************************************************************* 2013 INTERNATIONAL SUMMER SCHOOL ON TRENDS IN COMPUTING SSTiC 2013 Tarragona, Spain July 22-26, 2013 Organized by Rovira i Virgili University http://grammars.grlmc.com/SSTiC2013/ ********************************************************************* +++ next registration deadline: May 26 +++ ********************************************************************* AIM: SSTiC 2013 will be an open forum for the convergence of top class well recognized computer scientists and people at the beginning of their research career (typically PhD students) as well as consolidated researchers. SSTiC 2013 will cover the whole spectrum of computer science by means of 63 six-hour courses dealing with hot topics at the frontiers of the field. By actively participating, lecturers and attendees will share the idea of scientific excellence as th</pre> GRLMC 2013-05-19T20:04:00 http://permalink.gmane.org/gmane.comp.mathematics.hol/2703 <pre>::: ECSCW 2013 ::: Doctoral Colloquium The 13th European Conference on Computer Supported Cooperative Work (ECSCW 2013) 21-25 September 2013, Paphos, Cyprus http://www.ecscw2013.org/ The ECSCW 2013 Doctoral Colloquium provides an opportunity for doctoral students to discuss their research in an international forum, under the guidance of a panel of experienced CSCW researchers. The Doctoral Colloquium will be held on Sunday the 22nd of September 2013 as part of the 13th European Conference on Computer Supported Cooperative Work in Paphos, Cyprus (http://www.ecscw2013.org). We invite students who are working in the broad field of CSCW to apply. The strongest candidates will be those students who have a well-established research proposal, have made some progress towards it, but are still on time to benefit from advice and feedback by peers and senior colleagues. Selected candidates will be expected to give short, informal presentations of their work during the Colloquium, to be followed by extensive group</pre> Announce Announcements 2013-05-19T10:23:52 http://permalink.gmane.org/gmane.comp.mathematics.hol/2702 <pre>*********************************************************************** JOINT CALL FOR PARTICIPATION 29th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIX) 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) 26th IEEE Computer Security Foundations Symposium (CSF 2013) June 23-30, 2013 New Orleans, USA http://www.cs.cornell.edu/Conferences/MFPS29/ http://lii.rwth-aachen.de/lics/lics13/ http://csf2013.seas.harvard.edu Accommodation deadline (conference rate): May 20, 2013 Early registration deadline: May 22, 2013 *********************************************************************** * DATES MFPS (June 23-25) LICS (June 24 [tutorials], June 25-28 [conference], June 28-29 [workshops]) CSF (June 26-28, June 29-30 [workshops]) * REGISTRATION (deadline for early registration: May 22, 2013) https://www.regonline.com/mfps_lics_csf * ACCOMMODATION (deadline for special rate: May 20, 2013) http://www.cs.cornell.edu/Conferences/MFPS29/accommodations</pre> Andrzej Murawski 2013-05-17T12:07:55 http://permalink.gmane.org/gmane.comp.mathematics.hol/2701 <pre>------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Jose A Martin 2013-05-17T11:03:32 http://permalink.gmane.org/gmane.comp.mathematics.hol/2699 <pre>I've run your code in Kananaskis 7 and applied e(RW_TAC std_ss [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,OUT_def,COUT_def,BIT_VAL_def,VALUE_def]); directly on your step case. Then I got 22 subgoals, which are much less than your case ... Still it is too many ... the subgoals mainly come from the combinations of the assumptions. But I doubt the correctness of "NADDER_IMP_def". Please check it. If you really want to involve the uncertain state, like `Z`, `U`, `W`, then the type of the signals should be changed. Good Luck, Liya Quoting Yuntao Peng &lt;pengyt19890703&lt; at &gt;gmail.com&gt;: </pre> Liya Liu 2013-05-16T14:36:31 http://permalink.gmane.org/gmane.comp.mathematics.hol/2698 <pre>--------------------------------------------------------------------------- COMPUTABILITY IN EUROPE 2013: The Nature of Computation Milan, Italy, July 1 - 5, 2013 CALL FOR PARTICIPATION Informal Presentation Deadline: 31 May 2013 Early Registration Deadline: 31 May 2013 http://cie2013.disco.unimib.it co-located with Unconventional Computation and Natural Computation 2013 http://ucnc2013.disco.unimib.it --------------------------------------------------------------------------- TUTORIAL SPEAKERS: Gilles Brassard (Universite de Montreal) and Grzegorz Rozenberg (Leiden Institute of Advanced Computer Science and University of Colorado at Boulder) PLENARY TALKS: Ulle Endriss (University of Amsterdam) Lance Fortnow (Georgia Institute of Technology) Anna Karlin (University of Washington) Bernard Moret (Ecole Polytechnique Federale de Lausanne) Mariya So</pre> S B Cooper 2013-05-16T12:06:38 http://permalink.gmane.org/gmane.comp.mathematics.hol/2697 <pre>I am practicing using HOL4. As a beginner, a lot of primary problems puzzle me. There is the code of n-bit adder I writed according the paper of "Hardware verification using higher-order logic". I have proved the basis case, and stopped at the step case. set_trace "Unicode" 0; show_assums:=true; open HolKernel boolLib Parse bossLib; open listTheory; load "listlib"; open listlib; open arithmeticTheory; (***********************************************************************) (* *) (* n-bit adder *) (* *) (* Data structure: *) (* First input: bool list *) (* Second input: bool list *) (* Carry input: bool *) (* Sum output: bool list *) (* Carry output: bool *) (* *) (***********************************************************************) (***********************************************************************) (* Get the n-th element of the bool </pre> Yuntao Peng 2013-05-16T13:11:31 http://permalink.gmane.org/gmane.comp.mathematics.hol/2696 <pre>The talks at NFM 2013 will be webcast live starting May 14th, 8:00 AM Pacific Standard Time. All the NFM 2013 talks can be viewed at http://www.ustream.tv/channel/nasa-arc The program for NFM 2013 is available at http://ti.arc.nasa.gov/events/nfm-2013/program/ Neha --- To opt-out from this mailing list, send an email to fm-announcements-request&lt; at &gt;lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner&lt; at &gt;lists.nasa.gov ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d </pre> Rungta, Neha S. (ARC-TI)[Stinger Ghaffarian Technologies Inc. (SGTInc.)] 2013-05-14T13:28:17 http://permalink.gmane.org/gmane.comp.mathematics.hol/2695 <pre>Functions in HOL are (total) functions in the mathematical sense. They can't throw exceptions because they don't "do" anything; they are just a map from the domain type to the range type. If you want to model exceptions, you have various options, the simplest of which is probably to use the option type. I.e. define NTH_BIT_VAL : num -&gt; num list -&gt; num option, so that it returns NONE if the index is too large, otherwise it returns SOME x, where x is the desired element of the list. You may as well just use the EL constant already defined in listTheory. Define `NTH_BIT_VAL n ls = if n &lt; LENGTH ls then SOME (EL n ls) else NONE`; On Tue, May 14, 2013 at 4:46 AM, Yuntao Peng &lt;pengyt19890703&lt; at &gt;gmail.com&gt;wrote: ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a si</pre> Ramana Kumar 2013-05-14T10:01:57 http://permalink.gmane.org/gmane.comp.mathematics.hol/2694 <pre>A number list stored a set of numbers, the number value may be 0 or 1, no other case, now, I want to get the value of n-th element of the list. If n is greater than the length of the list,then fail. I don't know how to throw the exception which defined by myself. The function defined as follows: val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l l)) else (failwith "n is greater than list's LENGTH")`; Exception raised at TotalDefn.Define: between line 40, character 31 and frag 0 row 0 col 137: at TotalDefn.defnDefine: The following variables are free in the right hand side of the proposed definition: "failwith" ! Uncaught exception: ! HOL_ERR val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l l)) else fail()`; Exception raised at TotalDefn.Define: on line 41, characters 30-159: at TotalDefn.defnDefine: The following variables are free in the right hand side of the proposed definition: "fail" ! Uncaught exception: ! HOL_ERR however, I define function u</pre> Yuntao Peng 2013-05-14T03:46:14 http://permalink.gmane.org/gmane.comp.mathematics.hol/2693 <pre>********************************************************************* *** Federated Conference on Rewriting, Deduction, and Programming *** *** RDP 2013 *** *** June 23 - June 28, 2013 *** *** Eindhoven, The Netherlands *** *** http://www.win.tue.nl/rdp2013/ *** *** *** *** CALL FOR PARTICIPATION *** *** *** ********************************************************************* ************* EARLY REGISTRATION CLOSES ON JUNE 1 ************* --------------------------------------------------------------------- </pre> Luca Paolini 2013-05-14T07:53:45 http://permalink.gmane.org/gmane.comp.mathematics.hol/2692 <pre>Vince and Freek, I was wrong and you were right! First I used Vince's let get = Obj.magic o Toploop.getvalue;; but then I switched over to Freek's much more complicated exec_thm, as I could not see how to test for theorems with get, as I didn't know how to handle a get exception. My low-tech solution using the reference theorems of database.ml fell apart as soon as I wanted to refer to a theorem I proved. That would probably require the techniques of update_database.ml, similar to yours and Freek's: let exec = ignore o Toploop.execute_phrase false Format.std_formatter o !Toploop.parse_toplevel_phrase o Lexing.from_string;; [...] Obj.magic (Toploop.getvalue "buf__");; [...] let env = Obj.magic !Toploop.toplevel_env in I'm including my new code, hoping that someone knows how to simplify Freek's work with the simple get, and maybe to admit that my code might end up as complicated as Freek's miz3.ml or John's mizar.ml. That's OK as long as I can read it: my aim was only to get modify mi</pre> Bill Richter 2013-05-12T23:04:56 http://permalink.gmane.org/gmane.comp.mathematics.hol/2691 <pre>[ NOTE: We have delayed our submission dates by a week to bring ourselves into line with our co-conference, APLAS. Come to sunny Australia to escape the northern winter! ] CALL FOR PAPERS =============== Third International Conference on Certified Programs and Proofs (CPP 2013) -------------------------------------------------------------------------- December 2013, Australia (co-located with APLAS 2013) CPP is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. We invite submissions on topics that fit under this rubric. The first two CPP conferences were held in Kenting, Taiwan, and Kyoto, Japan, in December 2011 and 2012, respectively. As with the first meetings, the proceedings will be published in Springer-Verla</pre> Michael Norrish 2013-05-10T06:46:48 http://permalink.gmane.org/gmane.comp.mathematics.hol/2690 <pre>(* Apologies for multiple copies *) ------------------------------------------------------------------- FINAL CALL FOR PAPERS ------------------------------------------------------------------- The 5th International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2013) Part of CICM-2013, at University of Bath, UK 8-12th of July 2013 ------------------------------------------------------------------- Important Dates --------------- * Paper submission: *Mon May 27 2013* * Notification of acceptance: Mon June 10 2013 * Camera ready copy due: Mon June 17 2013 Invited Speakers ----------------- * Conor McBride, University of Strathclyde * Gilles Dowek, INRIA * Edwin Brady, University of St Andrews * Serge Mechveliani, Russian Academy of Science Program Committee ----------------- * David Aspinall, University of Edinburgh, UK * Serge Autexier, DKFI Bremen, Germany * Jacques Carette, McMaster U</pre> Iain Whiteside 2013-05-09T10:34:50 http://permalink.gmane.org/gmane.comp.mathematics.hol/2689 <pre>Here's a reasonable version of a miz3 interface for HOL Light. Thanks to Vince, Freek and Petros for helping me out! I believe this is the end of this parser-based discussion, so allow me to summarize. It's good for formal proofs to readable, especially if you want to attract mathematicians. John has always pushed for readable proofs, and writes in his purple FOL book that we should really be doing both declarative and procedural proofs, as neither is powerful enough. But it's also be nice for the Ocaml interface code to be readable, so it can be modified. I think my code below is much more readable that John's mizar.ml or Freek's masterpiece miz3.ml, whose interface I have tried to emulate. </pre> Bill Richter 2013-05-09T09:08:28 http://permalink.gmane.org/gmane.comp.mathematics.hol/2688 <pre>Thanks, Ramana! I think it would be good to compare what I'm doing with how things are in HOL4, because 1) John has always stressed the importance of readability in formal proofs, and 2) my code looks like it will be a lot simpler than John's mizar.ml or Freek's miz.ml. I know nothing of HOL4, and there is a lot I don't know in general, so you can teach me a lot. As you expressed reservations about the theorems assoc list in database.ml, tell me how DB.fetch is implemented. You can't detect matching braces with regular expressions. Thanks! I looked at your link, and I'll study it later. I think I realized that for the emulating the miz3 code that I've actually written, I don't actually need this, so I'll write that version first. What you probably need is to define your tactic language with a grammar and write a parser for it. I think I'm done with the HOL Light campl parser, and that Vince already told me everything I need. There's a line else if c = ";" then "parse_qproof \""^(S</pre> Bill Richter 2013-05-08T14:12:54 http://permalink.gmane.org/gmane.comp.mathematics.hol/2687 <pre>Unsubscribe: https://lists.cs.columbia.edu/cucslists/listinfo/memocode Unsubscribe: &amp;lt;mailto:memocode-unsubscribe&lt; at &gt;lists.cs.columbia.edu&gt; CALL FOR PAPERS - MEMOCODE 2013 (NOTE: NEW EXTENDED DATES for PAPERS and DESIGN CONTEST) Eleventh ACM/IEEE International Conference on Formal Methods and Models for Codesign http://www.memocode-conference.com 18-20 October 2013, Portland, Oregon, USA Co-located with DIFTS and FMCAD SCOPE The eleventh ACM/IEEE MEMOCODE conference focuses on research and developments in methods, tools, and architectures for the design of hardware/software systems. MEMOCODE seeks submissions that present novel formal methods and design techniques to create, refine, and verify complex hardware/software systems and to tackle the tight constraints on timing, power, costs, reliability and security that these systems face. We also invite application-oriented papers, and especially encourage submissions that highlight the tools and design perspect</pre> Marly Roncken 2013-05-06T22:25:05 http://permalink.gmane.org/gmane.comp.mathematics.hol/2686 <pre>Unsubscribe: https://lists.cs.columbia.edu/cucslists/listinfo/memocode Unsubscribe: &amp;lt;mailto:memocode-unsubscribe&lt; at &gt;lists.cs.columbia.edu&gt; Hi all, I would like to let you know that the MEMOCODE Design Contest for this year is coming up soon, on May 15. More details are available at http://memocode.irisa.fr/2013/competition.html Looking forward to your participation! Regards, Eriko Nurvitadhi Design Contest Chair _______________________________________________ Memocode mailing list Memocode&lt; at &gt;lists.cs.columbia.edu------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. This 200-page book is written by three acclaimed leaders in the field. The early access version is available now. Download your free book today! http://p.sf.net/sfu/neotech_d2d_may_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net</pre> Nurvitadhi, Eriko 2013-05-06T13:38:49 http://permalink.gmane.org/gmane.comp.mathematics.hol/2685 <pre>FMCAD 2013 - FORMAL METHODS IN COMPUTER-AIDED DESIGN FINAL CALL FOR PAPERS International Conference on Formal Methods in Computer-Aided Design http://www.fmcad.org/FMCAD13 Portland, OR, USA October 20-23, 2013 IMPORTANT DATES Abstract Submission: May 8 Paper Submission: May 15 Author Notification: July 17 Final Version: August 14 Conference: October 20 - 23 Student Forum: (NEW! --- See below for details) Submission Deadline: June 2 Notification: August 4 KEYNOTES - Pranav Ashar, Chief Technology Officer, Real Intent, "Static Verification Based Signoff - A Key Enabler for Managing Verification Complexity in the Modern SoC" - Lori A. Clarke, Professor, University of Massachusetts, Amherst, "Using Process Modeling and Analysis Techniques to Reduce Errors in Healthcare" TUTORIALS - Rajeev Alur, University of Pennsylvania, "Computer Augmented Program Engineering" - Jim Grundy, Intel Corporation, "Firmware Validation: Challenges and Opportunities" - Somesh Jha, Bill Harris, Tom Reps, U</pre> Chao Yan 2013-05-07T03:18:43 Search the mailing list at Gmane query http://search.gmane.org/?group=$group=gmane.comp.mathematics.hol