http://blog.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 research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical framework. The broad subject areas of LFMTP'13 are: * Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * New theory contributions: canonical frameworks, contextual frameworks, functional programming over logical frameworks. This year's invited speaker are Dale Miller (Inria) and Robert Harper (CMU) . In addition, this year LFMTP will celebrate the twenty years anniversary of the publication of: Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993 Program Committee: ================= * David Baelde, ENS * James Cheney, Edinburgh * Adam Chlipala, MIT * Dan Licata, CMU/IAS * Alberto Momigliano, Milano (organizer) * Brigitte Pientka, McGill (organizer) * Nicolas Pouillard ITU * Randy Pollack, Harvard (organizer) * Andrei Popescu, TUM * Florian Rabe, Bremen * Stephanie Weirich, UPenn Submission Details: ============ In addition to regular papers, we also solicit "work in progress" report, in a broad sense. Those do not need to report original or fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGPLAN style guidelines (9pt format, more details appear on the symposium web page). The length is restricted to 12 pages, except for "Work in Progress" papers, which are restricted to 6 pages. Submission is via EasyChair: https://www.easychair.org/conferences/?conf=lfmtp2013 Proceedings: ============ Accepted (regular) papers will be included in the ACM Digital Library. Authors are encouraged to publish auxiliary material with their paper (technical appendixes, source code, scripts, test data, etc.). Travel Support: =============== Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC program, see its web page (http://www.sigplan.org/PAC.htm). ------------------------------------------------------------------------------ Try New Relic Now &amp; We'll Send You this Cool Shirt New Relic is the only SaaS-based application performance monitoring service that delivers powerful full stack analytics. Optimize and monitor your browser, app, &amp; servers with just a few lines of code. Try New Relic and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_may_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </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 ones that are suggested for formal adoption by the OpenMath Society. IMPORTANT DATES (all times are "anywhere on earth") * 7 June: Submission * 20 June: Notification of acceptance or rejection * 5 July: Final revised papers due * 10 July: Workshop SUBMISSIONS Submission is via EasyChair (http://www.easychair.org/conferences?conf=om20131). Final papers must conform to the EasyChair LaTeX style. Initial submissions in this format are welcome but not mandatory – but they should be in PDF and within the given limit of pages/words. Submission categories: * Full paper: 5–10 EasyChair pages * Short paper: 1–4 EasyChair pages * CD description: 1-6 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 1-10 EasyChair pages (as appropriate w.r.t. the background knowledge required); a .zip or .tgz file of any related implementation (e.g. a Relax NG schema) should be attached. If not in EasyChair format, 500 words count as one page. PROCEEDINGS Electronic proceedings will be published with CEUR-WS.org. ORGANISATION COMMITTEE * Christoph Lange (University of Birmingham, UK) * James Davenport (University of Bath, UK) * Michael Kohlhase (Jacobs University Bremen, Germany) PROGRAMME COMMITTEE * Lars Hellström (Umeå Universitet, Sweden) * Jan Willem Knopper (Technische Universiteit Eindhoven, Netherlands) * Paul Libbrecht (Center for Educational Research in Mathematics and Technology, Martin-Luther-University Halle-Wittenberg) (to be completed) Comments/questions/enquiries: to be sent to openmath-workshop&lt; at &gt;googlegroups.com </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 the main motto of their research work. ADDRESSED TO: Graduate students from around the world. There are no pre-requisites in terms of the academic degree the attendee must hold. However, since there will be several levels among the courses, in the description of some of them reference may be made to specific knowledge background. SSTiC 2013 is appropriate also for people more advanced in their career who want to keep themselves updated on developments in the field. Finally, senior researchers will find it fruitful to listen and discuss with people who are main references of the diverse branches of computing nowadays. REGIME: 7 parallel sessions will be held during the whole event. Participants will be able to freely choose the courses they will be willing to attend as well as to move from one to another. VENUE: Palau Firal i de Congressos de Tarragona Arquitecte Rovira, 2 43001 Tarragona http://www.palaucongrestgna.com COURSES AND PROFESSORS: Divyakant Agrawal (Santa Barbara) [intermediate] Scalable Data Management in Enterprise and Cloud Computing Infrastructures Shun-ichi Amari (Riken) [introductory] Information Geometry and Its Applications James Anderson (Chapel Hill) [intermediate] Scheduling and Synchronization in Real-Time Multicore Systems Pierre Baldi (Irvine) [intermediate] Big Data Informatics Challenges and Opportunities in the Life Sciences Yoshua Bengio (Montréal) [introductory/intermediate] Deep Learning of Representations Stephen Brewster (Glasgow) [advanced] Multimodal Human-Computer Interaction Bruno Buchberger (Linz) [introductory] Groebner Bases: An Algorithmic Method for Multivariate Polynomial Systems. Foundations and Applications Rajkumar Buyya (Melbourne) [intermediate] Cloud Computing Jan Camenisch (IBM Zurich) [intermediate] Cryptography for Privacy Jeffrey S. Chase (Duke) [intermediate] Trust Logic as an Enabler for Secure Federated Systems Larry S. Davis (College Park) [intermediate] Video Analysis of Human Activities Paul De Bra (Eindhoven) [intermediate] Adaptive Systems Marco Dorigo (Brussels) [introductory] An Introduction to Swarm Intelligence and Swarm Robotics Paul Dourish (Irvine) [introductory] Ubiquitous Computing in a Social Context Max J. Egenhofer (Maine) [introductory/intermediate] Qualitative Spatial Relations: Formalizations and Inferences Richard M. Fujimoto (Georgia Tech) [introductory] Parallel and Distributed Simulation David Garlan (Carnegie Mellon) [advanced] Software Architecture: Past, Present and Future Mario Gerla (Los Angeles) [intermediate] Vehicle Cloud Computing Georgios B. Giannakis (Minnesota) [advanced] Sparsity and Low Rank for Robust Data Analytics and Networking Ralph Grishman (New York) [intermediate] Information Extraction from Natural Language Francisco Herrera (Granada) [intermediate] Imbalanced Classification: Current Approaches and Open Problems Paul Hudak (Yale) [introductory] Euterpea: From Signals to Symphonies Using Haskell Niraj K. Jha (Princeton) [intermediate] FinFET Circuit Design George Karypis (Minnesota) [introductory] Introduction to Parallel Computing: Architectures, Algorithms, and Programming Aggelos K. Katsaggelos (Northwestern) [intermediate/advanced] Sparsity-based Advances in Image Processing Arie E. Kaufman (Stony Brook) [advanced] Advances in Visualization Carl Kesselman (Southern California) [intermediate] Biomedical Informatics and Big Data Hugo Krawczyk (IBM Research) [intermediate] An Introduction to the Design and Analysis of Authenticated Key Exchange Protocols Pierre L'Ecuyer (Montréal) [intermediate] Quasi-Monte Carlo Methods in Simulation: Theory and Practice Laks Lakshmanan (British Columbia) [intermediate/advanced] Information and Influence Spread in Social Networks Wenke Lee (Georgia Tech) [introductory] DNS-based Monitoring of Malware Activities Maurizio Lenzerini (Roma La Sapienza) [intermediate] Ontology-based Data Integration Ming C. Lin (Chapel Hill) [introductory/intermediate] Physically-based Modeling and Simulation Jane W.S. Liu (Academia Sinica) [intermediate] Critical Information and Communication Technologies for Disaster Preparedness and Response Satoru Miyano (Tokyo) [intermediate] How to Hack Cancer Systems with Computational Methods Aloysius K. Mok (Austin) [intermediate] From Real-time Systems to Cyber-physical Systems Hermann Ney (Aachen) [intermediate/advanced] Probabilistic Modelling for Natural Language Processing - with Applications to Speech Recognition, Handwriting Recognition and Machine Translation Cathleen A. Norris (North Texas) &amp; Elliot Soloway (Ann Arbor) [introductory] Primary &amp; Secondary Educational Computing in the Age of Mobilism Jeff Offutt (George Mason) [intermediate] Cutting Edge Research in Engineering of Web Applications David Padua (Urbana) [intermediate] Parallel Programming with Abstractions Bijan Parsia (Manchester) [introductory] The Semantic Web: Conceptual and Technical Foundations Massoud Pedram (Southern California) [intermediate] Energy Efficient Architectures and Information Processing Systems Charles E. Perkins (FutureWei) [intermediate/advanced] Beyond 4G Prabhakar Raghavan (Google) [introductory/intermediate] Web Search and Advertising Sudhakar M. Reddy (Iowa) [introductory] Design for Test and Test of Digital VLSI Circuits Phillip Rogaway (Davis) [introductory/intermediate] Provably Secure Symmetric Encryption Gustavo Rossi (La Plata) [intermediate] Topics in Model Driven Web Engineering Kaushik Roy (Purdue) [introductory/intermediate] Low-energy Computing Robert Sargent (Syracuse) [introductory] Validating Models Douglas C. Schmidt (Vanderbilt) [intermediate] Patterns and Frameworks for Concurrent and Networked Software Bart Selman (Cornell) [intermediate] Fast Large-scale Probabilistic and Logical Inference Methods Mubarak Shah (Central Florida) [intermediate/advanced] Visual Crowd Surveillance Ron Shamir (Tel Aviv) [introductory] Revealing Structure in Disease Regulation and Networks Satinder Singh (Ann Arbor) [introductory/advanced] Reinforcement Learning: On Machines Learning to Act from Experience Dawn Xiaodong Song (Berkeley) [introductory] Selected Topics in Computer Security Mike Thelwall (Wolverhampton) [introductory] Sentiment Strength Detection for the Social Web Julita Vassileva (Saskatchewan) [introductory/intermediate] Engaging Users in Social Computing Systems Philip Wadler (Edinburgh) [introductory] Topics in Lambda Calculus and Life Yao Wang (Polytechnic New York) [introductory/advanced] Video Compression: Fundamentals and Recent Development Gio Wiederhold (Stanford) [introductory] Software Economics: How Do the Results of the Intellectual Efforts Enter the Global Market Place Limsoon Wong (National Singapore) [introductory/intermediate] The Use of Context in Gene Expression and Proteomic Profile Analysis Michael Wooldridge (Oxford) [introductory] Autonomous Agents and Multi-Agent Systems Ronald R. Yager (Iona) [introductory/intermediate] Fuzzy Sets and Soft Computing Philip S. Yu (Illinois Chicago) [advanced] Mining Big Data REGISTRATION: It has to be done at http://grammars.grlmc.com/SSTiC2013/Registration.php Since the capacity of the venue is limited, registration requests will be processed on a first come first served basis. The registration period will be closed when the capacity of the venue will be complete. FEES: They are the same (a flat rate) for all people by the corresponding deadline. They give the right to attend all courses. ACCOMMODATION: Information about accommodation is available on the website of the School. CERTIFICATE: Participants will be delivered a certificate of attendance. IMPORTANT DATES: Announcement of the programme: January 26, 2013 Six registration deadlines: February 26, March 26, April 26, May 26, June 26, July 26, 2013 QUESTIONS AND FURTHER INFORMATION: Lilica Voicu: florentinalilica.voicu&lt; at &gt;urv.cat POSTAL ADDRESS: SSTiC 2013 Research Group on Mathematical Linguistics (GRLMC) Rovira i Virgili University Av. Catalunya, 35 43002 Tarragona, Spain Phone: +34-977-559543 Fax: +34-977-558386 ACKNOWLEDGEMENTS: Ajuntament de Tarragona Diputació de Tarragona Universitat Rovira i Virgili ------------------------------------------------------------------------------ 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> 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 discussion in a friendly and constructive workshop. To apply please submit the following documents 1) A 4-page overview of your doctoral research, stating your research questions, level of advancement, and expected contributions. Formatting instructions and paper templates are available at http://ecscw2013.cs.ucy.ac.cy/templates.zip. The submissions are not anonymous and should therefore include names, affiliations and contact information. 2) A short (2-3 paragraph) biography. 3) A paragraph that articulates what you expect to gain from attending the ECSCW 2013 Doctoral Colloquium. 4) An email letter from your supervisor indicating that they support your application to the ECSCW 2013 Doctoral Colloquium and that they agree that your research is at an appropriate stage for participation. These letters should also indicate how you and other students might benefit from your participation in the colloquium. The e-mail should be sent to ecscw13dc&lt; at &gt;umbc.edu stating "ECSCW Doctoral Colloquium: + YOUR NAME" in the subject heading. All items should be submitted as PDF files through easychair https://www.easychair.org/conferences/?conf=ecscw2013 Item 1 should be submitted separately, items 2 and 3 should be submitted as a single PDF file. IMPORTANT DATES ·Submission Deadline: 15 June 2013 (5:00pm PDT) using EasyChair ·Notification Date: 22 June 2013 ·Camera-Ready Deadline: 26 September 2013 DC CHAIRS Antonella De Angeli, University of Trento, Trento, Italy Wayne Lutters, University of Maryland, Baltimore County, USA Contact: ecscw13dc&lt; at &gt;umbc.edu -------------------------------------------------------------------- This is not SPAM. If you want to be removed from this list, please send an email to [announce&lt; at &gt;cs.ucy.ac.cy] with the single word 'remove' in the subject of the email. ------------------------------------------------------------------------------ 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> 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.htm http://lii.rwth-aachen.de/lics/lics13/accomm.html http://csf2013.seas.harvard.edu/accomm.html * AFFILIATED WORKSHOPS CSF Foundations of Computer Security (FCS) http://prosecco.gforge.inria.fr/personal/bblanche/fcs13/ Socio-Technical Aspects in Security (STAST 2013) http://www.stast2013.uni.lu Formal and Computational Cryptography (FCC 2013) http://www.lsv.ens-cachan.fr/Events/FCC2013/ LICS Higher-Order Program Analysis (HOPA) http://hopa.cs.rhul.ac.uk Natural Language and Computer Science (NLCS) http://www.indiana.edu/~iulg/nlcs.html Foundations of Computer Security (FCS) http://prosecco.gforge.inria.fr/personal/bblanche/fcs13/ Syntax and Semantics of Low-Level Languages (LOLA) http://research.microsoft.com/en-us/events/lola2013/ ------------------------------------------------------------------------------ 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> 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 Soskova (Sofia University) Endre Szemeredi (Hungarian Academy of Sciences, Rutgers University) SPECIAL SESSIONS: * Algorithmic Randomness (organizers: Mathieu Hoyrup, Andre Nies) Speakers: Johanna Franklin (University of Connecticut, USA), Noam Greenberg (Victoria University, New Zealand), Joseph S. Miller (University of Wisconsin, USA), Nikolay Vereshchagin (Moscow State University, Russia) * Computational Complexity in the Continuous World (organizers: Akitoshi Kawamura, Robert Rettinger) Speakers: Mark Braverman (Princeton University, USA), Daniel S. Graca (Universidade do Algarve), Joris van der Hoeven (Ecole polytechnique, France), Chee K. Yap (New York University, USA) * Computational Molecular Biology (organizers: Alessandra Carbone, Jens Stoye) Speakers: Sebastian Boecker (University of Jena, Germany), Marilia D. V. Braga (Inmetro, Brazil), Andrea Pagnani (Human Genetics Foundation, Italy), Laxmi Parida (IBM Thomas J. Watson Research Center, USA) * Computation in Nature (organizers: Mark Daley, Natasha Jonoska) Speakers: Jerome Durand-Lose (Univ. of Orleans, France), Giuditta Franco (Univ. of Verona Italy), Lila Kari (Univ. of Western Ontario, Canada), Darko Stefanovic (Univ. of New Mexico, USA) * Data Streams and Compression (organizers: Paolo Ferragina, Andrew McGregor) Speakers: Graham Cormode (AT&amp;T Labs, USA), Irene Finocchi (University of Rome, Italy), Andrew McGregor (University of Massachusetts, USA), Marinella Sciortino (University of Palermo, Italy). * History of Computation (organizers: Gerard Alberts, Liesbeth De Mol) Speakers: David Alan Grier (George Washington University, USA), Thomas Haigh (University of Wisconsin, USA), Ulf Hashagen (Deutsches Museum, Germany), Matti Tedre (Stockholm University, Sweden). CiE serves as an interdisciplinary forum for research in all aspects of computability and foundations of computer science, as well as the interplay of these theoretical areas with practical issues in computer science and with other disciplines such as biology, mathematics, philosophy, or physics. Women in Computability Workshop, July 2, 2013: We continue the programme "Women in Computability" supported by the journal "Annals of Pure and Applied Logic" (Elsevier). Speakers: Irene Finocchi, Laxmi Parida, Liesbeth De Mol The Women in Computability workshop aims to bring together women in Computing and Mathematical research to present and exchange their academic and scientific experience with young researchers. The meeting will offer the CIE scientific community the opportunity to encourage young students, especially young female researchers, to have active careers in the mathematical and computational sciences. INFORMAL PRESENTATIONS: Continuing the tradition of past CiE conferences, this year's CiE conference endeavours to get the best of both worlds. In addition to the formal presentations based on our LNCS proceedings volume, we invite researchers to present informal presentations. For this, please send us a brief description of your talk (between one paragraph and one page) by the DEADLINE: MAY 31, 2013 Please submit your abstract electronically, via EasyChair &lt;https://www.easychair.org/login.cgi?conf=cie2013&gt;, selecting the category "Informal Presentation". You will be notified whether your talk has been accepted for informal presentation usually within a week after your submission. **** Also authors of abstracts accepted for presentation are invited to submit a paper extending the abstract to the journal Computability **** __________________________________________________________________________ ASSOCIATION COMPUTABILITY IN EUROPE http://www.computability.org.uk CiE Conference Series http://www.illc.uva.nl/CiE CiE 2013 http://cie2013.disco.unimib.it CiE Membership Application Form http://www.cs.swan.ac.uk/acie __________________________________________________________________________ ------------------------------------------------------------------------------ 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> 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 list *) (***********************************************************************) val NTH_BIT_def = Define `(NTH_BIT(n:num,[]) = F) /\ (NTH_BIT(0,l:bool list) = HD l) /\ (NTH_BIT(n:num,l:bool list) = NTH_BIT(n-1,TL l))`; (***********************************************************************) (* Computing value of the n-th element of the list *) (* ture then 1,or 0 *) (***********************************************************************) val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:bool list) = if(NTH_BIT(n,l)) then 1 else 0`; (***********************************************************************) (* Computing value of the bool element *) (* ture then 1,or 0 *) (***********************************************************************) val BIT_VAL_def = Define `BIT_VAL(aBIT:bool) = if(aBIT) then 1 else 0`; (***********************************************************************) (* Computing value of the whole list *) (***********************************************************************) val VALUE_def = Define `(VALUE(0,l:bool list) = NTH_BIT_VAL(0,l)) /\ (VALUE(SUC n:num,l:bool list)= (2 ** (SUC n)) * NTH_BIT_VAL(n,l) + VALUE(n,l))`; (***********************************************************************) (* Sum output of the n-th bit *) (***********************************************************************) val OUT_def = Define`OUT(n,inp1,inp2,cn,out) = (NTH_BIT(n,out) = (~NTH_BIT(n,inp1) /\ ~NTH_BIT(n,inp2) /\ cn) \/ (~NTH_BIT(n,inp1) /\ NTH_BIT(n,inp2) /\ ~cn) \/ (NTH_BIT(n,inp1) /\ ~(NTH_BIT(n,inp2)) /\ ~cn) \/ (NTH_BIT(n,inp1) /\ NTH_BIT(n,inp2) /\ cn))`; (***********************************************************************) (* Carry of the n-th bit *) (***********************************************************************) val COUT_def = Define`COUT(n,inp1,inp2,cn,cout) = (cout = (NTH_BIT(n,inp1) /\ NTH_BIT(n,inp2)) \/ (NTH_BIT(n,inp1) /\ cn) \/ (NTH_BIT(n,inp2) /\ cn))`; (***********************************************************************) (* The implementation of (n+1)-th full adder *) (***********************************************************************) val FULL_ADDER_IMP_def = Define`FULL_ADDER_IMP(SUC n,inp1,inp2,cn,out,cout) = (OUT(n,inp1,inp2,cn,out) /\ COUT(n,inp1,inp2,cn,cout))`; (***********************************************************************) (* Implementation of n-bit adder *) (***********************************************************************) val NADDER_IMP_def = Define`(NADDER_IMP(0,inp1,inp2,cin,out,cout) = (cout = cin)) /\ (NADDER_IMP(SUC n,inp1,inp2,cin,out,cout) = (?cn:bool. NADDER_IMP(n,inp1,inp2,cin,out,cn) /\ FULL_ADDER_IMP(SUC n,inp1,inp2,cn,out,cout)))`; (***********************************************************************) (* Specification of n-bit adder *) (***********************************************************************) val NADDER_SPEC_def = Define`NADDER_SPEC(SUC n,inp1,inp2,cin,out,cout) = ((2**(SUC n))*BIT_VAL(cout) + VALUE(n,out) = VALUE(n,inp1)+VALUE(n,inp2)+BIT_VAL(cin))`; (***********************************************************************) (* Main goal *) (***********************************************************************) g`!n:num inp1:bool list inp2:bool list cin:bool out:bool list cout:bool.((LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ (LENGTH inp1 &gt; n) /\ NADDER_IMP(SUC n,inp1,inp2,cin,out,cout)) ==&gt; NADDER_SPEC(SUC n,inp1,inp2,cin,out,cout)`; (***********************************************************************) (* Basis case *) (***********************************************************************) e(Induct); e(REPEAT GEN_TAC THEN REWRITE_TAC [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,BIT_VAL_def,OUT_def,COUT_def,VALUE_def]); e(SIMP_TAC bool_ss []); e(Cases_on `cin`); e(Cases_on `inp1`); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(RW_TAC list_ss []); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(Cases_on `h`); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(Cases_on `inp1`); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(RW_TAC list_ss []); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(Cases_on `h`); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); (***********************************************************************) (* Step case *) (***********************************************************************) e(REPEAT GEN_TAC); e(REWRITE_TAC [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,OUT_def,COUT_def,BIT_VAL_def,VALUE_def]); We will simple the goal as follows. Question 1:How to eliminate the existential quantifier "cn"? Question 2:How to use the following assumption in the hypothesis list? !inp1 inp2 cin out cout. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==&gt; NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) I do not know how to apply the tactic to the assumption. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; SUC n /\ (?cn. (?cn'. NADDER_IMP (n,inp1,inp2,cin,out,cn') /\ (NTH_BIT (n,out) &lt;=&gt; ~NTH_BIT (n,inp1) /\ ~NTH_BIT (n,inp2) /\ cn' \/ ~NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) /\ ~cn' \/ NTH_BIT (n,inp1) /\ ~NTH_BIT (n,inp2) /\ ~cn' \/ NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) /\ cn') /\ (cn &lt;=&gt; NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) \/ NTH_BIT (n,inp1) /\ cn' \/ NTH_BIT (n,inp2) /\ cn')) /\ (NTH_BIT (SUC n,out) &lt;=&gt; ~NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) /\ cn \/ ~NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) /\ ~cn \/ NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) /\ ~cn \/ NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) /\ cn) /\ (cout &lt;=&gt; NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) \/ NTH_BIT (SUC n,inp1) /\ cn \/ NTH_BIT (SUC n,inp2) /\ cn)) ==&gt; (2 ** SUC (SUC n) * (if cout then 1 else 0) + (2 ** SUC n * NTH_BIT_VAL (n,out) + VALUE (n,out)) = 2 ** SUC n * NTH_BIT_VAL (n,inp1) + VALUE (n,inp1) + (2 ** SUC n * NTH_BIT_VAL (n,inp2) + VALUE (n,inp2)) + if cin then 1 else 0) ------------------------------------ !inp1 inp2 cin out cout. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==&gt; NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) : proof So, I try to apply RW_TAC to the goal,then get 64 subgoals. e(RW_TAC list_ss [BIT_VAL_def,OUT_def,COUT_def,VALUE_def,NTH_BIT_def,NTH_BIT_VAL_def,NADDER_SPEC_def,NADDER_IMP_def,FULL_ADDER_IMP_def]); The subgoal at the top goal stack as follows. VALUE (n,out) + (2 ** SUC n + 2 ** SUC (SUC n)) = VALUE (n,inp1) + (VALUE (n,inp2) + (2 * 2 ** SUC n + 1)) ------------------------------------ 0. !inp1 inp2 cin out cout. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==&gt; NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) 1. NTH_BIT (n,out) 2. NTH_BIT (n,inp1) 3. NTH_BIT (n,inp2) 4. LENGTH inp1 = LENGTH inp2 5. LENGTH inp2 = LENGTH out 6. LENGTH inp1 &gt; SUC n 7. NADDER_IMP (n,inp1,inp2,T,out,T) 8. NTH_BIT (SUC n,out) &lt;=&gt; ~NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) \/ NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) 9. NTH_BIT (SUC n,inp1) 10. NTH_BIT (SUC n,inp2) : proof I can not move forward. thx! ------------------------------------------------------------------------------ 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> 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 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> 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 using ML, done. - fun nth_bit_val n l = if(n=0) then fail() else l; thx ------------------------------------------------------------------------------ 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> 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 miz3 to use tactics proofs instead of the unordered by list. Progress report: I still haven't coded up SUBGOAL_THEN, needed when a proof is quite long, and haven't handled terms which are lists, as they have semicolons. But I ported the first 185 lines of proofs in RichterHilbertAxiomGeometry/FontHilbertAxiom.ml, so I think the code below is solid. </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-Verlag’s Lecture Notes in Computer Science series. Suggested, but not exclusive, specific topics of interest for submissions include: certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; program logics, type systems, and semantics for certified code; certified decision procedures, mathematical libraries, and mathematical theorems; proof assistants and proof theory; new languages and tools for certified programming; program analysis, program verification, and proof-carrying code; certified secure protocols and transactions; certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; certificates for program termination; logics for certifying concurrent and distributed programs; higher-order logics, logical systems, separation logics, and logics for security; teaching mathematics and computer science with proof assistants; and “Proof Pearls” (elegant, concise, and instructive examples). Important Dates: ++++++++++++++++ Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a URL where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT). ============================ ========================== **Abstract Deadline:** Friday, June 7, 2013 **Submission Deadline:** Friday, June 14, 2013 **Author Notification:** Monday, August 26, 2013 **Camera-ready Papers Due:** Monday, September 16, 2013 ============================ ========================== Submission Instructions: ++++++++++++++++++++++++ Papers should be submitted electronically online via the conference submission web page at URL: http://www.easychair.org/conferences/?conf=cpp2013 Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. The proceedings of the symposium will be published as a volume in Springer-Verlag’s Lecture Notes in Computer Science series. Submission instructions including LaTeX style files are available from the CPP 2013 website. Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. *Papers not conforming to the above requirements concerning format and length may be rejected without further consideration.* The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference. Organisation ++++++++++++ :Program Co-Chairs: Georges Gonthier (Microsoft Research Cambridge) &amp; Michael Norrish (NICTA) :General Chair: Peter Schachte, *University of Melbourne* :Website: http://cpp2013.forge.nicta.com.au Program Committee ^^^^^^^^^^^^^^^^^ ========================= ======================================= Derek Dreyer MPI-SWS William Farmer McMaster University Jean-Christophe Filliâtre INRIA Cédric Fournet Microsoft Research Cambridge Benjamin Grégoire INRIA Reiner Hähnle Technische Universität Darmstadt Aquinas Hobor National University of Singapore Gyesik Lee Hankyong National University Cesar Muñoz NASA Langley Toby Murray NICTA Gopalan Nadathur University of Minnesota Claudio Sacerdoti Coen University of Bologna Peter Sewell University of Cambridge Bas Spitters University of Nijmegen Gang Tan Lehigh University Alwen Tiu Australian National University Yih-Kuen Tsay National Taiwan University Lihong Zhi Academia Sinica ========================= ======================================= ------------------------------------------------------------------------------ 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 https://lists.sourceforge.net/lists/listinfo/hol-info </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 University, Canada * Claudio Sacerdoti Coen, University of Bologna, Italy * Gudmund Grov, Heriot Watt University, UK * Cezar Ionescu, Potsdam Institute, Germany * Ewen Maclean, University of Edinburgh, UK * Florian Rabe (co-chair), Jacobs University, Germany * Tim Sheard, Portland State University, USA * Sergei Soloviev, IRIT, France * Stephen Watt, University of Western Ontario, Canada * Makarius Wenzel, Université Paris-Sud, France * Iain Whiteside (co-chair), University of Newcastle, UK * Freek Wiedijk, Radboud University, Netherlands * Wolfgang Windsteiger, RISC, Austria PLMMS Scope ----------- The program committee welcomes submissions on programming language issues related to all aspects of mechanised mathematics systems (MMS). In particular: - Mathematical algorithms - Tactics and proof search - Proofs - Mathematical notation Of particular interest are the dimensions of: - Expressiveness - Efficiency - Correctness - Understandability and Usability - Modularity and Extensibility - Design and implementation Mechanised mathematics systems, whether stand-alone or embedded in larger systems, include but are not limited to: - Dependent typed programming languages - Proof assistants - Computer algebra systems - Proof planning systems - Theorem proving systems - Theory formation systems These issues have a very colourful history. Why are all the languages of mainstream computer algebra systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical computer algebra systems? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modelling? How can MMS regain the upper hand on issues of "genericity" and "modularity"? What are the biggest barriers when using more mainstream languages for computer algebra systems, proof assistants or theorems provers? Many programming language innovations appeared in either computer algebra or proof systems first, before migrating into more mainstream programming languages. This workshop is an opportunity to present the latest innovations in the design of MMS that may be relevant to future programming languages, or conversely novel programming language principles that improve upon the implementation and deployment of MMS. Submission Details ------------------ Papers should be submitted via the PLMMS 2013 easychair website: https://www.easychair.org/conferences/?conf=plmms2013 Submissions must describe original unpublished work which is not been submitted for publication elsewhere. At least one author of each accepted paper is expected to attend PLMMS 2013 and present her or his paper. We wish to be flexible with paper length and will accept papers between 4 and 15 pages in length, submitted in PDF format. We invite submissions of both work-in-progress and fully polished research. All papers should be prepared in LaTeX and formatted according to the requirements of Springer's LNCS series. The corresponding style files can be downloaded from: http://www.springer.com/computer/lncs/lncs+authors Papers will be reviewed by at least three reviewers. Informal workshop proceeding will be circulated as a technical report and on CEUR-WS. Links ----- * https://www.easychair.org/conferences/?conf=plmms2013 abstract and paper submission webpage * http://www.springer.com/computer/lncs/lncs+authors submission style guide * http://www.cicm-conference.org/2013/cicm.php?event=plmms&amp;menu=general the PLMMS 2013 web site * http://www.cicm-conference.org/2013/cicm.php the CICM 2013 conference web siteThe University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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 https://lists.sourceforge.net/lists/listinfo/hol-info </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 \""^(String.escaped s)^"\"" in quotexpander in system.ml, and I just write one line let parse_qproof s = (String.sub s 1 (String.length s - 1));; Now every back-quoted expression `;[...]` becomes a string with no newline or bacsklash problems. Following Freek's miz3.ml, an entire theorem/proof will be such an expression `;[...]`, and I'll just write code to turn this string into a HOL Light proof. That doesn't sound very hard to me, but maybe it is, as I'm not done yet. But maybe I'm missing something, because I don't know what tactic language, grammar or parser means. I looked at your link and got confused right away! I know about syntax and semantics, but grammar is something different! I'll try to learn it about grammar. You're going down a route that I think many people do by accident and end up in a dead end or with a broken solution. Thanks for the warning. Maybe it would be more helpful if you told me how I'm replicating work that's already been done in HOL and HOL Light, so I can profit from this work instead of reinventing the wheel. HOL4 does not have a separate tactic language. Proof scripts are written in SML directly. (The SML implementation will have a parser etc. though.) HOL4 does have a sophisticated parser for the object language of HOL terms and types, which I think I've mentioned before. I don't know what this means, but it sounds relevant and important. </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 perspective of formal methods and models, including success as well as failure stories, constructive analysis thereof, and demonstrations of hardware/software codesign. Techniques may range from formal verification to simulation-based verification technologies, and from languages to design paradigms that unify hardware and software codesign. Architectures may range from cloud computing and multi-core platforms to networks on chip. Applications and demonstrators may address values ranging from productivity and reuse to performance and quality. MEMOCODE 2013 is co-located with FMCAD, the thirteenth conference on Formal Methods in Computer-Aided Design, and DIFTS, the International Workshop on Design and Implementation of Formal Tools and Systems. PAPER SUBMISSIONS Paper submissions must be accepted through the EasyChair review system on our web site. Papers must be 10 pages or less, and must be formatted following IEEE Computer Society guidelines. Submissions must be written in English, describe original work, and not substantially overlap papers that have been published or are being submitted to a journal or another conference with published proceedings. (NOTE: NEW, EXTENDED DATES !!!) Abstract submission deadline: May 15 Paper submission deadline: May 22 Notification of acceptance: June 18 Final version for Papers: July 17 DESIGN CONTEST MEMOCODE 2013 is proud to organize its traditional Design Contest. The conference will sponsor at least one prize with a significant monetary award. Each team delivering a complete and working solution will be invited to prepare a 2-page abstract to be published in the proceedings and to present it during a dedicated poster session at the conference. The winning teams may contribute a 4-page short paper for presentation in the conference program. Further information will be made available on our website. (NOTE: NEW, EXTENDED DATES !!!) Design Contest start: June 1 Design submission deadline: July 1 Notification of design results: July 19 Final version for abstracts: July 31 PUBLICATION Conference proceedings will be published by the IEEE Computer Society. Besides conference proceedings, we are planning a special journal issue with the very best 2013 papers of MEMOCODE, DIFTS, and FMCAD. We look forward to your participation! Marly Roncken, Jean-Pierre Talpin, and Eriko Nurvitadhi MEMOCODE 2103 Program Chairs and 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 https://lists.sourceforge.net/lists/listinfo/hol-info </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 https://lists.sourceforge.net/lists/listinfo/hol-info </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, University of Wisconsin-Madison, "Secure Programs via Game-Based Synthesis" - Other Tutorials TBD CONFERENCE SCOPE FMCAD 2013 is the thirteenth in a series of conferences on the theory and application of formal methods in hardware and system design and verification. FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing novel methods, technologies, theoretical results, and tools for formal reasoning about computing systems, as well as open challenges therein. FMCAD 2013 will be held in Portland, OR, USA, and co-located with MEMOCODE, the ACM/IEEE International Conference on Formal Methods and Models for Codesign, and DIFTS 2013, the International Workshop on Design and Implementation of Formal Tools and Systems. DIFTS will be held on October 19. MEMOCODE will take place from October 18 to 19, followed by a joint FMCAD/MEMOCODE tutorial day on October 20. FMCAD will continue from October 21 to 23, 2013. TOPICS OF INTEREST FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods technology and its application to computer-aided design. Topics of interest include, but are not limited to, the following: - Advances in model checking, theorem proving, equivalence checking, abstraction and reduction techniques, compositional methods, automatic decision procedures at the bit- and word-level, probabilistic methods, and combinations of deductive methods and decision procedures. - Topics related to the application of formal and semi-formal methods to functional and non-functional specification and validation of hardware and software. This includes timing and power modeling, and verification of computing systems on all levels of abstraction. System-level design and verification, especially for embedded systems, HW/SW co-design and verification, and transaction-level verification. - Modeling and specification languages, formal semantics of known languages or their subsets, model-based design, design derivation and transformation, and correct-by-construction methods. - Experience with the application of formal and semi-formal methods to industrial-scale designs. Tools that represent formal verification enablement, new features, or a substantial improvement in the automation of formal methods. - Application of formal methods in new areas. SUBMISSIONS Submissions must be made electronically in PDF format via EasyChair. More details are available from the FMCAD Web site. The proceedings will be freely available from the FMCAD Web site. Two categories of papers can be submitted: regular papers (8 pages), containing original research; and short papers (4 pages), containing emerging results, practical experiences or original ideas that can be described succinctly. Regular and short papers must use the IEEE Transactions format on letter-size paper with a 10-point font size, see http://www.ieee.org/portal/pages/pubs/transactions/stylesheets.html. We recommend that self-citations be written in the third person. Submissions must contain original research that has not been previously published, nor concurrently submitted for publication. Any partial overlap with any published or concurrently submitted paper must be clearly indicated. If experimental results are reported, authors are strongly encouraged to provide adequate access to their data so that results can be independently verified. A small number of accepted papers will be considered for a distinguished paper award. PUBLICATION Accepted papers, both regular and short, will be published in the FMCAD Conference Proceedings. We expect to have ACM In-Cooperation Status and IEEE Technical Co-Sponsorship, as has been the case with previous FMCAD conferences. FMCAD and authors will share the copyright for accepted papers and we plan on publishing the proceedings in the ACM Digital Library and in IEEE Xplore. As with recent editions of FMCAD, the papers are also expected to be available online from the FMCAD Web page. In addition, we are planning a special journal issue with the best papers of FMCAD, DIFTS, and MEMOCODE 2013. STUDENT FORUM FMCAD 2013 will host a Student Forum that provides a platform for graduate students at any career stage to introduce their research to the wider Formal Methods community, and solicit feedback. Submissions for the event must be short reports describing research ideas or ongoing work that the student is currently pursuing, and must be within the scope of FMCAD. Work, part of which has been previously published, will be considered; the novel aspect to be addressed in future work must be clearly described in such cases. The event will consist of short presentations by the student authors of each accepted submission, and of a poster that will be on display throughout the duration of the conference. Accepted submissions will be listed, with title and author name, in the event description in the conference proceedings. The authors will also have the option to upload their poster and presentation to the FMCAD webpage. Limited funds will be available for travel assistance for students with accepted contributions. CO-LOCATED EVENTS The following meetings will be co-located with this year's edition: - MEMOCODE 2013, the ACM/IEEE International Conference on Formal Methods and Models for Codesign (http://www.memocode-conference.com). - DIFTS 2013, International Workshop on Design and Implementation of Formal Tools and Systems We are also proud to host this year's Hardware Model Checking Competition (HWMCCC 2013). ORGANIZING COMMITTEE CHAIRS Barbara Jobstmann, Jasper Design Automation and CNRS-VERIMAG Sandip Ray, Intel Corporation LOCAL ARRANGEMENT CHAIR Joe Leslie-Hurd, Intel Corporation PUBLICATION CHAIR Julien Schmaltz, Open University of The Netherlands TUTORIAL CHAIR Malay Ganai, NEC Laboratories America STUDENT FORUM CHAIR Thomas Wahl, Northeastern University PUBLICITY CHAIR Chao Yan, Intel Corporation WEBMASTER Shilpi Goel, University of Texas at Austin PROGRAM COMMITTEE Jason Baumgartner, IBM Corporation Dirk Beyer, University of Passau Armin Biere, Johannes Kepler University Per Bjesse, Synopsys Nikolaj Bjorner, Microsoft Research Roderick Bloem, TU Graz Gianpiero Cabodi, Politecnico di Torino Hana Chockler, IBM Research Alessandro Cimatti, FBK-irst Koen Claessen, Chalmers University of Technology Malay Ganai, NEC Labs America Steven German, IBM Ganesh Gopalakrishnan, University of Utah Alberto Griggio, FBK-IRST Ziyad Hanna, University of Oxford Keijo Heljanko, Aalto University Alan Hu, University of British Columbia William Hung, Synopsys Inc Warren Hunt, University of Texas Susmit Jha, Strategic CAD Lab, Intel Shuvendu Lahiri, Microsoft Research Panagiotis Manolios, Northeastern University Tom Melham, University of Oxford John O'Leary, Intel Corporation Lee Pike, Galois, Inc. Ruzica Piskac, Max Planck Institute for Software Systems (MPI-SWS) Philipp Ruemmer, Uppsala University, Department of Information Technology Cesar Sanchez, IMDEA Software Institute Julien Schmaltz, Open University of The Netherlands Natasha Sharygina, University of Lugano, Switzerland Anna Slobodova, Centaur Technology Niklas Sorensson, Mentor Graphics Daryl Stewart, ARM Thomas Wahl, Northeastern University Georg Weissenbacher, Vienna University of Technology STEERING COMMITTEE Jason Baumgartner, IBM, USA Armin Biere, Johannes Kepler University in Linz, Austria Aarti Gupta, NEC Labs America, USA Warren Hunt, University of Texas at Austin, USA Panagiotis Manolios, Northeastern University, USA ------------------------------------------------------------------------------ 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 </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