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

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

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

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

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

_{Nov}

_{Dec}

From: Yves Bertot <Yves.B<ertot@in...>  20160920 12:37:58

CPP 2017: The 6th ACM SIGPLAN Conference on Certified Programs and Proofs Paris, France, January 16  17, 2017 (colocated with POPL'17) http://cpp2017.mpisws.org/ Call for papers 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 welcome submissions in research areas related to formal certification of programs and proofs. The following is a suggested list of topics of interests to CPP. This is a nonexhaustive list and should be read as a guideline rather than a requirement.  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 proofcarrying 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 semidecision procedures, including equality, firstorder logic, and higherorder unification;  certificates for program termination;  logics for certifying concurrent and distributed programs;  higherorder logics, logical systems, separation logics, and logics for security;  teaching mathematics and computer science with proof assistants. Submission guidelines Papers should be submitted in PDF format through the EasyChair submission page at https://easychair.org/conferences/?conf=cpp2017. Submitted papers must be formatted following the ACM SIGPLAN Proceedings format (seehttp://www.sigplan.org/Resources/Author/) using **10 point** font for the main text (not the default 9pt font). Papers should should not exceed **12 pages** including all tables, figures, and bibliography. Shorter papers are very welcome and will be given equal consideration. Abstracts must be submitted by October 5, 2016 (AOE). The deadline for full papers is October 12, 2016 (AOE), and authors have the option to withdraw their papers during the window between the two. Submissions must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. They 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 nonspecialist. Technical and formal developments directed to the specialist should follow. 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. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Dafny, Elf, HOL, HOLLight, Isabelle, Lean, Matita, Mizar, NQTHM, PVS, Vampire, etc. Such formal developments must be submitted together with the paper as auxiliary material, and will be taken into account during the reviewing process. 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 welcome. One author of each accepted paper is expected to present it at the conference. For any questions about the formatting or submission of papers, please consult the PC chairs. Important Dates Abstract submission: October 5, 2016 Full paper submission: October 12, 2016 Notification: November 16, 2016 Conference dates: January 1617, 2017 Program Committee Reynald Affeldt, AIST, Japan Thorsten Altenkirch, University of Nottingham, UK Jesús Aransay, Universidad de La Rioja, Spain Andrea Asperti, University of Bologna, Italy Clark Barrett, Stanford University, USA Yves Bertot, INRIA, France (cochair) Nikolaj Bjorner, Microsoft Research, USA Ana Bove, Chalmers University of Technology & University of Gothenburg, Sweden Delphine Demange, IRISA / University of Rennes 1, France Reiner Hähnle, Technische Universität Darmstadt, Germany Marieke Huisman, University of Twente, Netherlands Cezary Kaliszyk, University of Innsbruck, Austria Robbert Krebbers, Aarhus University, Denmark Ondřej Kunčar, Technische Universität München, Germany Mohsen Lesani, MIT, USA Assia Mahboubi, INRIA, France Michael Norrish, Data61, Australia Vincent Rahli, University of Luxembourg, Luxembourg Tom Ridge, University of Leicester, UK Viktor Vafeiadis, MPISWS, Germany (cochair) Freek Verbeek, Open University of the Netherlands, Netherlands Steve Zdancewic, University of Pennsylvania, USA 
From: Adnan Rashid <adnan.rashid@se...>  20160919 11:30:31

Dear all, I am having a weird message persistently while loading the multivariate realanalysis theory in HOLLight. *Segmentation fault (core dumped)* This message appear after loading some of the theorems. I guess that this error may be due to my recent update of HOLLight sources from the github repositories. Is there any way around? I have another query. Can anybody know the way to reduce the loading time of HOLLight theories? Thanks and best regards.  Adnan Rashid PhD Candidate NUSTSEECS Islamabad, Pakistan 
From: Joao Marcos <botocudo@gm...>  20160916 22:28:21

(with apologies for multiple postings) TABLEAUX, FroCoS, ITP CALL FOR WORKSHOPS AND TUTORIALS Three of the main conferences on automated reasoning  TABLEAUX, FroCoS, and ITP  will be held in Brasilia, Brazil, between 25 and 29 September 2017. Following the long tradition of those events, we invite researchers and practitioners to submit proposals for colocated workshops and indepth tutorials on topics relating to automated theorem proving and its applications. Workshops/tutorials can target the automated reasoning community in general, focus on a particular theorem proving system, or highlight more specific issues or recent developments. Colocated events will take place between 23 and 24/25 September and will be held on the same premises as the main conference. Conference facilities are offered free of charge to the organisers. Workshop/tutorialonly attendees will enjoy a significantly reduced registration fee. Detailed organisational matters such as paper submission and review process, or publication of proceedings, are up to the organisers of individual workshops. All accepted workshops/tutorials will be expected to have their program ready by 18 August 2017. Proposals for workshops/tutorials should contain at least the following pieces of information:  name and contact details of the main organiser(s)  (if applicable:) names of additional organisers  title and organisational style of event (tutorial, public workshop, project workshop, etc.)  preferred length of workshop (between half day and two days)  estimated number of attendees  short (up to one page) description of topic  (if applicable:) pointers to previous editions of the workshop, or to similar events Proposals are invited to be submitted by email to nalon@..., no later than 9 December 2016. Selected events will be notified by 23 December 2016. The workshop/tutorial selection committee consists of the TABLEAUX, FroCoS, and ITP program chairs and the conference organisers. 
From: <geoff@cs...>  20160916 16:55:15

(with apologies for multiple postings) CALL FOR WORKSHOPS AND TUTORIALS Three of the main conferences on automated reasoning  TABLEAUX, FroCoS, and ITP  will be held in Brasilia, Brazil, between 25 and 29 September 2017. Following the long tradition of those events, we invite researchers and practitioners to submit proposals for colocated workshops and indepth tutorials on topics relating to automated theorem proving and its applications. Workshops/tutorials can target the automated reasoning community in general, focus on a particular theorem proving system, or highlight more specific issues or recent developments. Colocated events will take place between 23 and 24/25 September and will be held on the same premises as the main conference. Conference facilities are offered free of charge to the organisers. Workshop/tutorialonly attendees will enjoy a significantly reduced registration fee. Detailed organisational matters such as paper submission and review process, or publication of proceedings, are up to the organisers of individual workshops. All accepted workshops/tutorials will be expected to have their program ready by 18 August 2017. Proposals for workshops/tutorials should contain at least the following pieces of information:  name and contact details of the main organiser(s)  (if applicable:) names of additional organisers  title and organisational style of event (tutorial, public workshop, project workshop, etc.)  preferred length of workshop (between half day and two days)  estimated number of attendees  short (up to one page) description of topic  (if applicable:) pointers to previous editions of the workshop, or to similar events Proposals are invited to be submitted by email to nalon@..., no later than 9 December 2016. Selected events will be notified by 23 December 2016. The workshop/tutorial selection committee consists of the TABLEAUX, FroCoS, and ITP program chairs and the conference organisers. 
From: Dwi Teguh Priyantini <dwi.teguh51@ui...>  20160915 01:15:33

Dear all, Continuing my preveous question, I still need help related to my my master thesis's work. I wanted to verify the FPGA implementation of an arithmetic operation using VHDL in HOL Light. I need a standard arithmetic operations for classifier implementation in FPGA. Arithmetic operations that I want to verify is custom (not using libraries available), in order to better meet the needs of the application domain. For time efficiency, whether there is open access library or do I have to build from scratch? If I had to build from scratch, is there any suggestions on where I can get a proper reference? Because the reference I had (especially about embedding VHDL) is not freely accessible for me. Thank you. Best Regards, Dwi  Dwi Teguh Priyantini Fasilkom UI  1506782322 
From: Andrea Rosa <andrea.rosa@us...>  20160914 09:33:42

ICPE 2017 8th ACM/SPEC International Conference on Performance Engineering Sponsored by ACM SIGMETRICS, SIGSOFT, and SPEC RG L'Aquila, Italy April 2226, 2017 https://icpe2017.spec.org/  IMPORTANT DATES Research and Industrial / Experience Abstracts: Sep 23, 2016 Research and Industrial / Experience Papers: Sep 30, 2016 Research and Industrial / Experience Paper Notification: Nov 18, 2016 WorkinProgress/Vision Papers: Nov 25, 2016 Workshop Proposals: Nov 05, 2016 Workshop Proposal Notification: Nov 19, 2016 Dates for tutorials, posters and demos will be announced.  SCOPE AND TOPICS The goal of the International Conference on Performance Engineering (ICPE) is to integrate theory and practice in the field of performance engineering by providing a forum for sharing ideas and experiences between industry and academia. Nowadays, complex systems of all types, like Webbased systems, data centers and cloud infrastructures, social networks, peertopeer, mobile and wireless systems, cyberphysical systems, the Internet of Things, realtime and embedded systems, have increasingly distributed and dynamic system architectures that provide high flexibility, however, also increase the complexity of managing endtoend application performance. ICPE brings together researchers and industry practitioners to share and present their experiences, discuss challenges, and report stateoftheart and inprogress research on performance engineering of software and systems, including performance measurement, modeling, benchmark design, and runtime performance management. The focus is both on classical metrics such as response time, throughput, resource utilization, and (energy) efficiency, as well as on the relationship of such metrics to other system properties including but not limited to scalability, elasticity, availability, reliability, and security. This year's main theme is costeffective performance engineering, where cost has a wide interpretation including measures such as effort and energy in addition to traditional performance measures. Topics of interest include, but are not limited to: Performance modeling of software * Languages and ontologies * Methods and tools * Relationship/integration/tradeoffs with other QoS attributes * Analytical, simulation and statistical modeling methodologies * Model validation and calibration techniques * Automatic model extraction * Performance modeling and analysis tools Performance and software development processes/paradigms * Software performance patterns and antipatterns * Software/performance tool interoperability (models and data interchange formats) * Performanceoriented design, implementation and configuration management * Software Performance Engineering and ModelDriven Development * Gathering, interpreting and exploiting software performance annotations and data * System sizing and capacity planning techniques * (Modeldriven) Performance requirements engineering * Relationship between performance and architecture * Collaboration of development and operation (DevOps) for performance * Performance and agile methods * Performance in ServiceOriented Architectures (SOA) * Performance of microservice architectures and containers Performance measurement, monitoring and analysis * Performance measurement and monitoring techniques * Analysis of measured application performance data * Application tracing and profiling * Workload characterization techniques * Experimental design * Tools for performance testing, measurement, profiling and tuning Benchmarking * Performance metrics and benchmark suites * Benchmarking methodologies * Development of parameterizable, flexible benchmarks * Benchmark workloads and scenarios * Use of benchmarks in industry and academia Runtime performance management * Use of models at runtime * Online performance prediction * Autonomic resource management * Utilitybased optimization * Capacity management Power and performance, energy efficiency * Power consumption models and management techniques * Tradeoffs between performance and energy efficiency * Performancedriven resource and power management Performance modeling and evaluation in different environments and application domains * Webbased systems, ebusiness, Web services * Big data systems, data analytics systems, and other data analysis systems * Internet of Things * Social networks * Cyberphysical systems * Industrial Internet (Industry 4.0) * Virtualization and cloud computing * Autonomous/adaptive systems * Transactionoriented systems * Communication networks * Parallel and distributed systems * Embedded systems * Multicore systems * Cluster and grid computing environments * High performance computing * Eventbased systems * Realtime and multimedia systems * Peertopeer, mobile and wireless systems All other topics related to performance of software and systems.  SUBMISSION GUIDELINES Authors are invited to submit original, unpublished papers that are not being considered in another forum. A variety of contribution styles for papers are solicited including: basic and applied research papers for novel scientific insights, industrial and experience papers reporting on applying performance engineering or benchmarks in practice, and workinprogress/vision papers for ongoing but yet interesting work. Different acceptance criteria apply based on the expected content of the individual contribution types. Authors will be requested to selfclassify their papers according to topic and contribution style when submitting their papers. Submissions to all tracks need to be uploaded to ICPE's submission system and conform to the ACM submission format. For detailed submission instructions, please visit: https://icpe2017.spec.org/submissions.html. At least one author of each accepted paper is required to register at the full rate, attend the conference and present the paper. Presented papers will be published in the ICPE 2017 conference proceedings that will be published by ACM and included in the ACM Digital Library. After the conference, there will be a call for a special issue of a journal. AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.)  PROGRAM COMMITTEE (RESEARCH PAPERS) Amy Apon, Clemson University Martin Arlitt, HP Labs and University of Calgary Alberto Avritzer, Performance Engineering Consultant Steffen Becker, University of Technology Chemnitz Robert Birke, IBM Zurich Research Laboratory Andre B. Bondi, Software Performance and Scalability Consulting LLC Niklas Carlsson, Linkoping University Lydia Y. Chen, IBM Zurich Research Laboratory Lucy Cherkasova, HP Labs Antinisca Di Marco, Università dell'Aquila Wilhelm Hasselbring, Kiel University Alexandru Iosup, Delft University of Technology Evangelia Kalyvianaki, City University London Samuel Kounev, University of Wuerzburg Heiko Koziolek, ABB Corporate Research Diwakar Krishnamurthy, University of Calgary Patrick Lee, The Chinese University of Hong Kong Catalina M. Lladó, Universitat Illes Balears Lei Lu, VMware Andrea Marin, University of Venice Daniel Menasce, George Mason University Daniel S. Menasché, Federal Univ. of Rio de Janeiro José Merseguer, Universidad de Zaragoza Ningfang Mi, Northeastern University Raffaela Mirandola, Politecnico di Milano Manoj Nambiar, Tata Consultancy Services Dorina Petriu, Carleton University Denys Poshyvanyk, College of William and Mary Ralf Reussner, Karlsruhe Institute of Technology Alma Riska, Network Appliances Jerry Rolia, HP Labs Rekha Singhal, Tata Consultancy Services Mirco Tribastone, IMT Institute for Advanced Studies Catia Trubiani, Gran Sasso Science Institute Petr Tuma, Charles University Ana Lucia Varbanescu, University of Amsterdam Enrico Vicario, University of Florence Katinka Wolter, Freie Universitaet zu Berlin Murray Woodside, Carleton University Feng Yan, University of NevadaReno Xiaoyun Zhu, Futurewei Technologies Inc  ORGANIZING COMMITTEE General Chairs * Walter Binder, Università della Svizzera italiana (USI), Switzerland * Vittorio Cortellessa, Università dell'Aquila, Italy Research Program Chairs * Anne Koziolek, Karlsruhe Institute of Technology, Germany * Evgenia Smirni, College of William and Mary, USA Industry Program Chairs * Meikel Poess, Oracle, USA Tutorials Chair * Valeria Cardellini, Università di Roma Torvergata, Italy Workshops Chairs * Hanspeter Mössenböck, Johannes Kepler Universität Linz, Austria * Catia Trubiani, Gran Sasso Science Institute, Italy Posters and Demos Chair * Lubomir Bulej, Charles University, Czech Republic Awards Chairs * Petr Tuma, Charles University, Czech Republic * Murray Woodside, Carleton University, Canada Local Organization Chair * Antinisca Di Marco, Università dell'Aquila, Italy Publicity Chairs * Andrea Rosà, Università della Svizzera italiana (USI), Switzerland * Diego Perez, Politecnico di Milano, Italy Finance Chair * André van Hoorn, University of Stuttgart Publication and Registration Chair * Davide Arcelli, Università dell'Aquila, Italy Web Site Chair * Cathy Sandifer, SPEC, USA  Andrea Rosà PhD student  Teaching assistant Faculty of Informatics  2nd floor Università della Svizzera italiana (USI) Via G. Buffi 13 CH6904 Lugano Switzerland (e) andrea.rosa@...<mailto:andrea.rosa@...> (p) +41 58 666 4455 ext. 2183 (w) http://www.inf.usi.ch/phd/rosaa/ 
From: Ken Kubota <mail@ke...>  20160912 00:04:09

Dear Daniel de Rauglaudre, dear List Members, A mechanized proof (i.e., verified in the R0 implementation) of (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) avoiding any appeal to the Axiom of Choice is now available online at: http://www.kenkubota.de/files/R0_draft_excerpt_with_proof_of_K8033.pdf Instead of the Axiom of Choice, the (much weaker) Axiom of Descriptions is used. The Axiom of Descriptions for R0 is available online at: http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (p. 351 f.) The required theorem was theorem 5311 [cf. Andrews, 2002, p. 235] (which in turn requires the Axiom of Descriptions), not theorem 5312. Kind regards, Ken Kubota References Kubota, Ken (2015c), Proof of K8033. Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_proof_of_K8033.pdf (September 12, 2016). SHA512: 5864427d033e7135c17f3a5c88fefc70 4faa3a24c9e03ab2f6a5889b5012542e b83d7db208238bddce7344378afac81d 1f4cc3313b9e58f6009eae943a2d98b0. ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 > Anfang der weitergeleiteten Nachricht: > > Von: Ken Kubota <mail@...> > Betreff: Aw: [CoqClub] is the axiom of choice... ? > Datum: 11. September 2016 um 18:50:17 MESZ > An: coqclub@... > Kopie: holinfo@..., "Prof. Peter B. Andrews" <andrews@...> > Antwort an: coqclub@... > > Dear Daniel de Rauglaudre, > dear List Members, > > The proposition > (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) > you want to prove is very similar to an exercise in the main work of Andrews [cf. Andrews, 2002, p. 237 (X5308)], > AC^b → (∀ x, ∃ y, P x y) = ∃ f, ∀ x, P x (f x) > where it is the consequent of an implication, but using the (weaker) existential quantifier > instead of the uniqueness quantifier, and an equivalence instead of the implication, > and the antecedent of the implication is (an instantiation of) the Axiom of Choice. > > The two major logistic systems based on Church's simple theory of types [cf. Church, 1940] > are Mike Gordon's HOL and Peter B. Andrews' Q0, which differ in the treatment of the Axiom of Choice. > Mike Gordon's HOL implements the epsilon operator which requires the Axiom of Choice, > whereas Peter B. Andrews' Q0 implements the description operator, such that the Axiom of Choice can be avoided. > It should be noted that already Gordon himself wrote that "the [epsilon]operator looks rather suspicious". > Details are discussed at > https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00069.html > https://lists.cam.ac.uk/pipermail/clisabelleusers/2016September/msg00014.html > > Information on Mike Gordon's HOL is available in [Gordon/Melham, 1993] and at > https://holtheoremprover.org > which is a polymorphic version of Church's simple theory of types. > Descendants are Larry Paulson's Isabelle/HOL and John Harrison's HOL Light. > > Information on Peter B. Andrews' Q0 is available in [Andrews, 2002, pp. 210215] and at > http://plato.stanford.edu/entries/typetheorychurch/#ForBasEqu > which is, like Church's original theory, a simple type theory. > A descendant is R0, a dependent type theory (and an implementation), to be announced at > http://dx.doi.org/10.4444/100.10 > > Since you use a stronger hypothesis (involving the uniqueness quantifier), > I believe there is a possibility of proving your proposition without using the Axiom of Choice, > but requiring the Axiom of Descriptions only. The Axiom of Descriptions allows > one to extract the single element from a singleton (unit set). > At the very first glance, your proposition might be derivable from theorem 5312 > [cf. Andrews, 2002, p. 235]. > > > Kind regards, > > Ken Kubota > > > > References > > Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0120585359 > (Hardcover). ISBN 0120585367 (Paperback). > > Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: > Kluwer Academic Publishers. ISBN 1402007639. DOI: 10.1007/9789401599344. > > Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of > Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at > http://plato.stanford.edu/archives/spr2014/entries/typetheorychurch/ (July 2, > 2016). > > Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: > Journal of Symbolic Logic 5, pp. 5668. > > Gordon, Michael J. C., and Melham, Thomas F., eds. (1993), Introduction to HOL: > A theorem proving environment for higher order logic, Cambridge: Cambridge > University Press. ISBN 0521441897. > > Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, > 2015). Unpublished manuscript. SHA512: a0dfe205eb1a2cb29efaa579d68fa2e5 > 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 > 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: > http://dx.doi.org/10.4444/100.10 > > Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (p. 1, pp. 356364, pp. > 411420, and pp. 754755). Available online at > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf > (January 24, 2016). SHA512: 67a48ee12a61583bd82c286136459c0c > 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 > 3d1047d1831bc357eb57b263b44c885b. > > Kubota, Ken (2015b), Excerpt from [Kubota, 2015] (p. 1, pp. 165174, and pp. > 350352). Available online at > http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf > (August 13, 2016). SHA512: 8702d932d50f2e1f6b592dc03b6f283e > 64ba18f881150b4ae32e4b915249d241 3db34ba4c3dcf0e0cdef25b679d9615f > 424adb1803a179e578087ded31b573b9. > > ____________________ > > Ken Kubota > doi: 10.4444/100 > http://dx.doi.org/10.4444/100 > > > >> Am 11.09.2016 um 11:09 schrieb Daniel de Rauglaudre <daniel.de_rauglaudre@...>: >> >> Hi all, >> >> Is the axiom of choice required if all sets have one only element ? >> If not, how to prove it ? >> >> Russel said that if all sets contain a pair of socks, we need the axiom >> of choice to select a sock in each pair but that if they are shoes, >> we don't need it, because the choice function can be : "take the left >> shoe". >> >> But for sets of one only element ? >> >> Namely, I want to prove : >> (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) >> >> Is is possible, or do I need the […] axiom of choice ? >> >> Thanks. >> >>  >> Daniel de Rauglaudre >> http://pauillac.inria.fr/~ddr/ > 
From: Ken Kubota <mail@ke...>  20160911 17:08:03

Dear Daniel de Rauglaudre, dear List Members, The proposition (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) you want to prove is very similar to an exercise in the main work of Andrews [cf. Andrews, 2002, p. 237 (X5308)], AC^b → (∀ x, ∃ y, P x y) = ∃ f, ∀ x, P x (f x) where it is the consequent of an implication, but using the (weaker) existential quantifier instead of the uniqueness quantifier, and an equivalence instead of the implication, and the antecedent of the implication is (an instantiation of) the Axiom of Choice. The two major logistic systems based on Church's simple theory of types [cf. Church, 1940] are Mike Gordon's HOL and Peter B. Andrews' Q0, which differ in the treatment of the Axiom of Choice. Mike Gordon's HOL implements the epsilon operator which requires the Axiom of Choice, whereas Peter B. Andrews' Q0 implements the description operator, such that the Axiom of Choice can be avoided. It should be noted that already Gordon himself wrote that "the [epsilon]operator looks rather suspicious". Details are discussed at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00069.html https://lists.cam.ac.uk/pipermail/clisabelleusers/2016September/msg00014.html Information on Mike Gordon's HOL is available in [Gordon/Melham, 1993] and at https://holtheoremprover.org which is a polymorphic version of Church's simple theory of types. Descendants are Larry Paulson's Isabelle/HOL and John Harrison's HOL Light. Information on Peter B. Andrews' Q0 is available in [Andrews, 2002, pp. 210215] and at http://plato.stanford.edu/entries/typetheorychurch/#ForBasEqu which is, like Church's original theory, a simple type theory. A descendant is R0, a dependent type theory (and an implementation), to be announced at http://dx.doi.org/10.4444/100.10 Since you use a stronger hypothesis (involving the uniqueness quantifier), I believe there is a possibility of proving your proposition without using the Axiom of Choice, but requiring the Axiom of Descriptions only. The Axiom of Descriptions allows one to extract the single element from a singleton (unit set). At the very first glance, your proposition might be derivable from theorem 5312 [cf. Andrews, 2002, p. 235]. Kind regards, Ken Kubota References Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0120585359 (Hardcover). ISBN 0120585367 (Paperback). Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: Kluwer Academic Publishers. ISBN 1402007639. DOI: 10.1007/9789401599344. Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/archives/spr2014/entries/typetheorychurch/ (July 2, 2016). Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: Journal of Symbolic Logic 5, pp. 5668. Gordon, Michael J. C., and Melham, Thomas F., eds. (1993), Introduction to HOL: A theorem proving environment for higher order logic, Cambridge: Cambridge University Press. ISBN 0521441897. Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, 2015). Unpublished manuscript. SHA512: a0dfe205eb1a2cb29efaa579d68fa2e5 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: http://dx.doi.org/10.4444/100.10 Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (p. 1, pp. 356364, pp. 411420, and pp. 754755). Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (January 24, 2016). SHA512: 67a48ee12a61583bd82c286136459c0c 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 3d1047d1831bc357eb57b263b44c885b. Kubota, Ken (2015b), Excerpt from [Kubota, 2015] (p. 1, pp. 165174, and pp. 350352). Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (August 13, 2016). SHA512: 8702d932d50f2e1f6b592dc03b6f283e 64ba18f881150b4ae32e4b915249d241 3db34ba4c3dcf0e0cdef25b679d9615f 424adb1803a179e578087ded31b573b9. ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 > Am 11.09.2016 um 11:09 schrieb Daniel de Rauglaudre <daniel.de_rauglaudre@...>: > > Hi all, > > Is the axiom of choice required if all sets have one only element ? > If not, how to prove it ? > > Russel said that if all sets contain a pair of socks, we need the axiom > of choice to select a sock in each pair but that if they are shoes, > we don't need it, because the choice function can be : "take the left > shoe". > > But for sets of one only element ? > > Namely, I want to prove : > (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) > > Is is possible, or do I need the […] axiom of choice ? > > Thanks. > >  > Daniel de Rauglaudre > http://pauillac.inria.fr/~ddr/ 
From: GRLMC <grlmc@gr...>  20160910 15:12:45

LATA 2017: 2nd call for papers*To be removed from our mailing list, please respond to this message with UNSUBSCRIBE in the subject line* ************************************************************************* 11th INTERNATIONAL CONFERENCE ON LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS LATA 2017 Umeå, Sweden March 610, 2017 Organized by: Department of Computing Science Umeå University Research Group on Mathematical Linguistics (GRLMC) Rovira i Virgili University http://grammars.grlmc.com/LATA2017/ ************************************************************************* AIMS: LATA is a conference series on theoretical computer science and its applications. Following the tradition of the diverse PhD training events in the field organized by Rovira i Virgili University since 2002, LATA 2017 will reserve significant room for young scholars at the beginning of their career. It will aim at attracting contributions from classical theory fields as well as application areas. VENUE: LATA 2017 will take place in Umeå, a university town in North Sweden which was European Capital of Culture in 2014. The venue will be the Faculty of Science and Technology. SCOPE: Topics of either theoretical or applied interest include, but are not limited to: algebraic language theory algorithms for semistructured data mining algorithms on automata and words automata and logic automata for system analysis and programme verification automata networks automatic structures codes combinatorics on words computational complexity concurrency and Petri nets data and image compression descriptional complexity foundations of finite state technology foundations of XML grammars (Chomsky hierarchy, contextual, unification, categorial, etc.) grammatical inference and algorithmic learning graphs and graph transformation language varieties and semigroups languagebased cryptography mathematical and logical foundations of programming methodologies parallel and regulated rewriting parsing patterns power series string processing algorithms symbolic dynamics term rewriting transducers trees, tree languages and tree automata weighted automata STRUCTURE: LATA 2017 will consist of: invited talks peerreviewed contributions INVITED SPEAKERS: Franz Baader (Technical University of Dresden), Approximately Description Logics Thomas Eiter (Technical University of Vienna), tba Michael R. Fellows (University of Bergen), On Some Finiteness Theorems about Formal Languages Georg Gottlob (University of Oxford), Logic, Languages, and Rules for Web Data Extraction and Reasoning over Data Thomas Wilke (University of Kiel), Backward Deterministic omegaAutomata PROGRAMME COMMITTEE: Eric Allender (Rutgers University, Piscataway, US) Amihood Amir (BarIlan University, Ramat Gan, IL) Christel Baier (Technical University of Dresden, DE) Armin Biere (Johannes Kepler University Linz, AT) Avrim Blum (Carnegie Mellon University, Pittsburgh, US) Ondřej Bojar (Charles University in Prague, CZ) JinYi Cai (University of Wisconsin, Madison, US) Liming Cai (University of Georgia, Athens, US) Alessandro Cimatti (Bruno Kessler Foundation, Trento, IT) Rocco De Nicola (IMT School for Advanced Studies Lucca, IT) Rod Downey (Victoria University of Wellington, NZ) Frank Drewes (Umeå University, SE) Zoltán Fülöp (University of Szeged, HU) Gregory Z. Gutin (Royal Holloway, University of London, UK) Lane A. Hemaspaandra (University of Rochester, US) Dorit S. Hochbaum (University of California, Berkeley, US) Deepak Kapur (University of New Mexico, Albuquerque, US) Marek Karpinski (University of Bonn, DE) JoostPieter Katoen (RWTH Aachen University, DE) Evangelos Kranakis (Carleton University, Ottawa, CA) Lars M. Kristensen (Bergen University College, NO) Kim G. Larsen (Aalborg University, DK) Axel Legay (INRIA, Rennes, FR) Leonid Libkin (University of Edinburgh, UK) Carsten Lutz (University of Bremen, DE) João Marques Silva (University of Lisbon, PT) Carlos MartínVide (Rovira i Virgili University, Tarragona, ES, chair) Mitsunori Ogihara (University of Miami, Coral Gables, US) Arlindo Oliveira (Instituto Superior Técnico, Lisbon, PT) David Parker (University of Birmingham, UK) Madhusudan Parthasarathy (University of Illinois, UrbanaChampaign, US) Doron A. Peled (BarIlan University, Ramat Gan, IL) Dominique Perrin (ParisEst MarnelaVallée University, FR) JeanÉric Pin (Paris Diderot University, FR) Sanguthevar Rajasekaran (University of Connecticut, Storrs, US) Bruce Reed (McGill University, Montréal, CA) Wojciech Rytter (University of Warsaw, PL) Kunihiko Sadakane (University of Tokyo, JP) Davide Sangiorgi (University of Bologna, IT) Helmut Seidl (Technical University of Munich, DE) Jens Stoye (Bielefeld University, DE) WingKin Sung (National University of Singapore, SG) Dimitrios M. Thilikos (CNRS, LIRMM, FR & National and Kapodistrian University of Athens, GR) Ioannis G. Tollis (University of Crete, Heraklion, GR) Bianca Truthe (University of Giessen, DE) Frits Vaandrager (Radboud University, Nijmegen, NL) Rob van Glabbeek (CSIRO, Sydney, AU) ORGANIZING COMMITTEE: Yonas Demeke (Umeå) Frank Drewes (Umeå, cochair) Petter Ericson (Umeå) Anna Jonsson (Umeå) Carlos MartínVide (Tarragona, cochair) Manuel Jesús Parra Royón (Granada) Bianca Truthe (Giessen) Florentina Lilica Voicu (Tarragona) Niklas Zechner (Umeå) SUBMISSIONS: Authors are invited to submit nonanonymized papers in English presenting original and unpublished research. Papers should not exceed 12 singlespaced pages (including eventual appendices, references, proofs, etc.) and should be prepared according to the standard format for Springer Verlag's LNCS series (see http://www.springer.com/computer/lncs?SGWID=016467933410). Submissions have to be uploaded to: https://easychair.org/conferences/?conf=lata2017 PUBLICATIONS: A volume of proceedings published by Springer in the LNCS series will be available by the time of the conference. A special issue of the journal Information and Computation (Elsevier, 2015 JCR impact factor: 0.873) will be later published containing peerreviewed substantially extended versions of some of the papers contributed to the conference. Submissions to it will be by invitation. REGISTRATION: The registration form can be found at: http://grammars.grlmc.com/LATA2017/Registration.php DEADLINES (all at 23:59 CET): Paper submission: October 21, 2016 Notification of paper acceptance or rejection: November 25, 2016 Final version of the paper for the LNCS proceedings: December 5, 2016 Early registration: December 5, 2016 Late registration: February 20, 2017 Submission to the journal special issue: June 10, 2017 QUESTIONS AND FURTHER INFORMATION: florentinalilica.voicu (at) urv.cat POSTAL ADDRESS: LATA 2017 Research Group on Mathematical Linguistics (GRLMC) Rovira i Virgili University Av. Catalunya, 35 43002 Tarragona, Spain Phone: +34 977 559 543 Fax: +34 977 558 386 ACKNOWLEDGEMENTS: Umeå universitet Universitat Rovira i Virgili 
From: <geoff@cs...>  20160908 13:10:38

The 2nd Global Conference on Artificial Intelligence Berlin Germany, 29th September  2nd October 2016 http://easychair.org/smartprogram/GCAI2016/ Call for Participation The 2nd Global Conference on Artificial Intelligence (GCAI 2016) will be held at the Freie Universitaet Berlin from 29th September to 2nd October, 2016. The conference addresses all aspects of artificial intelligence. There will be 29 papers presented, tutorials on automated theorem proving in classical and non classical logic, and three invited speakers ... Simon Colton, Falmouth University, and Goldsmiths, University of London, UK Computational Creativity Daniel Lee, University of Pennsylvania, USA Robotics and Machine Learning Toby Walsh, TU Berlin, Germany and UNSW/Data61, Australia Will AI end Jobs, Wars or Humanity? The full program is available at http://easychair.org/smartprogram/GCAI2016/program.html Registration: http://easychair.org/smartprogram/GCAI2016/Registration.html GCAI is organized by LRG (http://www.lrg.global) and the Freie Universitaet Berlin. 
From: Damien Pous <Damien.P<ous@en...>  20160905 11:41:11

First Call for Papers  16th International Conference on RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMiCS 2017) May 1519, 2017 Lyon, France http://ramicsconference.org  GENERAL INFORMATION: For more than two decades, the RAMiCS conferences series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond. TOPICS: We invite submissions in the general field of algebraic structures relevant to computer science and on applications of such algebras. Topics of the conference include, but are not limited to the following theory * algebraic structures from semigroups, residuated lattices and semirings to Kleene algebras, relation algebras and quantales * other algebras relevant to the theory of automata, concurrency, formal languages, games, networks, programming languages and social choice * algorithmic, categorytheoretic, coalgebraic or prooftheoretic methods for such algebras * their formalisation with automated and interactive theorem provers applications * tools and techniques for the verification and correctness of sequential and concurrent programs * quantitative and qualitative models for computing systems * logics of programs, e.g., modal, dynamic, interval, temporal or resource logics, logics for games, social choice and distributed systems * design of algorithms, network protocol analysis, optimisation and control INVITED SPEAKERS: * Annabelle McIver (Macquarie University, Sydney * JeanEric Pin (CNRS, IRIF, Paris) * Alexandra Silva (University College, London) IMPORTANT DATES: Abstract Submission: 2016, Nov 25 Paper Submission: 2016, Dec 2 Author Notification: 2017, Feb 3 Cameraready papers: 2017, Feb 24 RAMiCS 2017: 2017, May 1519 SUBMISSION INSTRUCTIONS: Submission is via EasyChair at https://www.easychair.org/conferences/?conf=ramics16 All papers will be peer reviewed by at least three referees. The proceedings will be published in an LNCS volume by Springer, ready at the conference. Submissions must be in English, in PDF format and should not exceed 16 pages in LNCS style. Submissions must be unpublished, not under review for publication elsewhere and provide sufficient information to judge their merits. Additional material may be provided in a clearly marked appendix or by a reference to a manuscript on a web site. Experimental data, software or mathematical components for theorem provers must be available in sufficient detail for reviewers. Deviation from these requirements may lead to rejection. Accepted papers must be produced with LaTeX. One author of each accepted paper is expected to present the paper at the conference. Formatting instructions and LNCS style files can be obtained at: http://www.springer.de/comp/lncs/authors.html. COMMITTEES: Conference Chair: Damien Pous, CNRS, France Programme Chairs: Peter Höfner, NICTA, Australia Georg Struth, U Sheffield, UK, Programme Committee: Luca Aceto, Reykjavik U, Iceland Rudolf Berghammer, U Kiel, Germany Filippo Bonchi, CNRS, France Jules Desharnais, U Laval, Canada Hitoshi Furusawa, Kagoshima U, Japan Tim Griffin, U Cambridge, UK Walter Guttmann, U Canterbury, New Zealand Robin Hirsch, UCL, UK Peter Höfner, Data61, CSIRO, Australia Marcel Jackson, LaTrobe U, Australia JeanBaptiste Jeannin, Samsung, USA Peter Jipsen , Chapman U, USA Christian Johansen, U Oslo, Norway Wolfram Kahl, McMaster U, Canada Dexter Kozen, Cornell U, USA Szabolcs Mikulas, Birkbeck U, UK Bernhard Möller, U Augsburg, Germany José N. Oliveira, U Minho, Portugal Damien Pous, CNRS, France Georg Struth, U Sheffield, UK, Pascal Weil, CNRS, France Michael Winter, Brock U, Canada 
From: Ken Kubota <mail@ke...>  20160902 15:20:13

Dear Makarius Wenzel, dear Members of the Research Community, The "tradeoff" argument concerning the "tradeoff in theoretical simplicity versus complexity required for practical applications of logic" given at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00084.html reminds me of an email discussion I had with Larry Paulson about natural deduction vs. axiomatic (Hilbertstyle) deductive systems (with respect to automation). Of course, certain concessions cannot be avoided, and for automation, natural deduction (making metatheorems symbolically representable) is the only choice, although one would like to prefer a Hilbertstyle system in which all rules of inference can be reduced to a single one, like in Q0. Nevertheless, one has to be aware that concessions for practical reasons (e.g., automation) are deviations from the "pure" logic, and while deviations concerning certain decisions are necessary, for all other decisions, the original concept remains, and the general design decisions still apply. In the HOL handbook, this is reflected by Andrew Pitts' consideration regarding Q0: "From a logical point of view, it would be better to have a simpler substitution primitive, such as 'Rule R' of Andrews' logic Q0, and then to derive more complex rules from it." [Gordon/Melham, 1993, p. 213] https://sourceforge.net/p/hol/mailman/message/35287517/ What Andrews calls "expressiveness" [Andrews, 2002, p. 205], is what I, vice versa, call "reducibility", and this concept is already implicit in Church's work (the simple theory of types), in which reducibility is omnipresent either as Currying (reducing functions of more than one argument to functions with only one argument, due to Schoenfinkel, implemented via lambdaconversion) or as the definability of the logical connectives (reducing them to combinations of a small set of primitive symbols). Moreover, reducibility (expressiveness) is not just "theoretical simplicity". The reduction of symbols, variable binders, axioms, and rules of inference lays bare the inner logic of formal logic and mathematics, and reveals interdependencies between them. This holds for both interdependencies within each field (e.g., for rules: between primitive and derived rules, for symbols: between primitive and defined symbols, etc.) as well as interdependencies among the fields (e.g., the derivability of the rule of modus ponens from a certain set of rules and axioms). (Also independence: In Andrews' Q0, it is shown that elementary logic is independent of the Axiom of Choice, which is, in my opinion, a nonlogical axiom, like the Axiom of Infinity. In Gordon's HOL, this is not possible, since the use of the epsilon operator instead of the description operator makes the Axiom of Choice inevitable.) Exactly this  laying bare the inner logic of formal logic and mathematics  makes Church's and Andrews' formulations of the mathematical language so important, not only Church's (and Andrews') "precise formulation of the syntax" https://www.cl.cam.ac.uk/techreports/UCAMCLTR175.pdf (p. 5), which also is the result of consequently carrying out the principle of reducibility (expressiveness). Church's main achievement is the creation of a mathematical language largely following the concept of expressiveness/reducibility; whereas this concept seems to be implicit in the work of Church, it is explicit in the work of Andrews. Hence, while practical considerations enforce deviations from the "pure" logic, still implementations (e.g., Gordon's HOL or Isabelle/HOL) are based on and have to face comparison with the "pure" logical system (e.g., Q0). Therefore practical concessions are in some sense a layer on top of (or, "overloading") the "pure" logic in certain areas, but do not render the general concept of expressiveness (reducibility) irrelevant. So it is not simply an alternative between logical rigor and practical considerations, but the latter overrides the general concept in certain fields only. It is important to keep this root (i.e., the underlying, but partially covered concept) and its remaining validity in mind (e.g., the reducibility not of rules, but still of symbols, variable binders, and axioms; avoidance of the use of the Axiom of Choice by preferring the description operator to the epsilon operator). With the above quote from the documentation of the original (Gordon's) HOL system, this awareness is clearly expressed. Concerning "type class instantiation", my guess is that with dependent type theory, the more expressive mathematical language provides other means which might replace the features provided by the current Isabelle/HOL (polymorphic type theory). At least certain language features of the original (Gordon's) HOL system, such as a) the introduction (definition) of types [cf. Gordon/Melham, 1993, pp. 225 ff.; cf. paragraph 2.5.4 of http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf (pp. 38 ff.) ], b) or the use of compound types [cf. Gordon/Melham, 1993, p. 195; cf. paragraph 1.2 of http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf (p. 11)] can be expressed very naturally in the dependent type theory R0, and from its point of view, these HOL language features then appear as rather artificial extensions (even with the introduction of new axioms!) which were necessary to emulate some of the expressiveness of the language of dependent type theory with the limited means of the language of polymorphic type theory, and, hence, as a preliminary and auxiliary solution. Regarding the concerns about expanding abbreviations (definitions), this kind of argument is not applicable to all representations of logic. In the R0 implementation, formulae are represented as binary trees, each having assigned a natural number. So internally, any wellformed formula (wff) can be addressed by its number, and expansion (and definition) is only a question of parsing and printing, but not of the logical core (in which no definitions exist, but only binary trees and their numbers representing expanded wffs). Of course, due to Isabelle's concept of a metalogical framework, or other practical considerations, different circumstances may be relevant that I am not familiar with. For the HOL documentation team, it might be worth considering making the brilliant HOL documents, such as http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf available directly on the HOL homepage in order to make it readable within the browser, e.g., via https://holtheoremprover.org/documents/kananaskis10logic.pdf since a download is a barrier for many people, for example, due to security considerations, or at public terminals providing browsing, but not downloading. For references, please see: https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00069.html https://sourceforge.net/p/hol/mailman/message/35287517/ Kind regards, Ken Kubota ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 
From: Peter SchÃ¼ller <peter.schuller@ma...>  20160902 12:52:33

(Apologies if you receive multiple copies of this email. Please distribute to interested parties.) Call For Participation 32nd International Conference on Logic Programming New York City, USA October 1621, 2016 http://software.imdea.org/Conferences/ICLP2016/ *** Early registration deadline: September 5. *** News:  The list of accepted papers is available online: http://software.imdea.org/Conferences/ICLP2016/accepted.html  Invited talks: * Arun Majumdar: One Billion Dollars, Global Warming and Logic Programming. * Francesca Rossi: Embedding Ethical Principles in Decision Support Systems: Can (Constraint) Logic Programming Play a Role?  Tutorials: * Michael Kifer, Theresa Swift and Benjamin Grosof: Practical Knowledge Representation and Reasoning in Ergo. * Yuliya Lierler: Relating Constraint Answer Set Programming and Satisfiability Modulo Theories.  Autumn School on Computational Logic: http://iclp16school.webs.upv.es/ * Roman Bartak: Constraint Logic Programming * Veronica Dahl: Language processing through logic grammars and constraints * Torsten Schaub: Answer Set Programming: foundations and applications * C.R.Ramakrishnan: Verification and probabilistic logic programming  Sponsors: * The Association for Logic Programming: http://logicprogramming.org/ * LogicBlox, Inc: http://www.logicblox.com/ * Semantic Systems: http://www.semanticsystems.com/ * UT Dallas: http://www.utdallas.edu/ Conference Scope Since the first conference held in Marseille in 1982, ICLP has been the pre mier international conference for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to:  Theory: Semantic Foundations, Formalisms, Nonmonotonic Reasoning, Knowledge Representation.  Implementation: Compilation, Virtual Machines, Parallelism, Constraint Han dling Rules, Tabling.  Environments: Program Analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing.  Language Issues: Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, Programming Techniques.  Related Paradigms: Inductive and Coinductive Logic Programming, Constraint Logic Programming, AnswerSet Programming, SATChecking.  Applications: Databases, Big Data, Data Integration and Federation, Soft ware Engineering, Natural Language Processing, Web and Semantic Web, Agents, Artificial Intelligence, Bioinformatics, and Education. In addition to the presentations of accepted papers, the technical program will include invited talks, advanced tutorials, the doctoral consortium, and several workshops. Important Dates Early Registration Deadline: September 5, 2016 Conference: October 1621, 2016 Conference Organization General Chairs: Michael Kifer Stony Brook University, USA NengFa Zhou City University of New York, USA Program Chairs: Manuel Carro UPM and IMDEA Software Institute, Spain Andy King University of Kent, UK Workshop Chair: Marcello Balduccini Drexel University, USA Publicity Chair: Peter Schueller Marmara University, Turkey Doctoral Consortium Chairs: Marina De Vos University of Bath, UK Neda Saeedloei University of Minnesota Duluth, USA Programming Contest Chair: Paul Fodor Stony Brook University, USA Web Presence: Joaquin Arias IMDEA Software Institute, Spain Program Committee: Marcello Balduccini Drexel University, USA Mutsunori Banbara Kobe University, Japan Roman Bartak Charles University, Czech Republic Pedro Cabalar University of Corunna, Spain Mats Carlsson SICS, Sweden Manuel Carro UPM and IMDEA Software Institute, Spain Michael Codish BenGurion University of the Negev, Israel Marina De Vos University of Bath, UK Agostino Dovier Universita degli Studi di Udine, Italy Gregory Duck National University of Singapore, Singapore Esra Erdem Sabanci University, Turkey Wolfgang Faber University of Huddersfield, UK Thom Fruehwirth University of Ulm, Germany John Gallagher Roskilde University, Denmark, and IMDEA Software Institute, Spain Marco Gavanelli Universita degli Studi di Ferrara, Italy Martin Gebser University of Potsdam, Germany Michael Hanus CAU Kiel, Germany Katsumi Inoue NII, Japan Gerda Janssens KU Leuven  University of Leuven, Belgium Andy King University of Kent, UK Ekaterina Komendantskaya HeriotWatt University, UK Michael Leuschel University of Dusseldorf, Germany Vladimir Lifschitz University of Texas, USA Jose F. Morales IMDEA Software Institute, Spain Enrico Pontelli New Mexico State University, USA Jorg Puhrer Leipzig University, Germany Ricardo Rocha University of Porto, Portugal Zoltan Somogyi Independent Researcher, Australia Harald Sondergaard University of Melbourne, Australia Theresa Swift NOVALINKS, US, and UNL, Portugal Francesca Toni Imperial College London, UK Irina Trubitsyna University of Calabria, Italy Mirek Truszczynski University of Kentucky, USA Alicia Villanueva Universitat Politecnica de Valencia, Spain Jan Wielemaker VU University Amsterdam, Netherlands Stefan Woltran TU Wien, Austria Fangkai Yang Schlumberger Inc., USA JiaHuai You University of Alberta, Canada Workshops The ICLP 2016 program will include several workshops. They are perhaps the best places for the presentation of preliminary work, underdeveloped novel ideas, and new open problems to a wide and interested audience with opportuni ties for intensive discussions and project collaboration. Autumn School on Computational Logic Students and researchers are invited to participate in the Autumn School with the following tutorials: * Roman Bartak: Constraint Logic Programming * Veronica Dahl: Language processing through logic grammars and constraints * Torsten Schaub: Answer Set Programming: foundations and applications * C.R.Ramakrishnan: Verification and probabilistic logic programming Information on scholarships can be found on the homepage: http://iclp16school.webs.upv.es/ Doctoral Consortium The Twelfth Doctoral Consortium (DC) on Logic Programming provides research students with the opportunity to present and discuss their research direc tions, and to obtain feedback from both peers and experts in the field. Accepted participants will receive partial financial support to attend the event and the main conference. The best paper from the DC will be given the opportunity to present in a session of the main ICLP conference. Conference Venue The venue will be the Sheraton LaGuardia East Hotel in Flushing, New York City. New York City is an international tourist destination, receiving 56 million tourists in 2014 alone. Several sources have ranked New York the most photographed city in the world. Times square, known as the city's heart, is the brightly illuminated hub of the Broadway theatre district. The Statue of Liberty greets new arrivals to the Americas by ship in the late 19th and early 20th century, and is a globally recognized symbol of the United States. Flush ing is associated by many with the National Tennis Centre, since Flushing Meadows has been the home of the US Open Grand Slam tennis tournament every year since 1978. New York is the most populous city in the United States and one of the most populous urban agglomerations in the world. Situated in one of the world's largest natural harbours, New York City consists of five boroughs, each of which is a separate county of New York State. The conference hotel is situated in the Queens borough, just a twominute walk from the FlushingMain Street rail station. Direct train lines take you directly from there to Times Square in just over 45 minutes, which is fast for New York City. The Museum of Modern Art can be reached in under 40 mins, Grand Central Terminal in 40 mins, the Empire State Building under 50 mins, and The High Line Park in 50 minutes. The hotel is also close to LaGuardia Airports and JFK. LaGuardia is just 3 miles away and the hotel offers a complementary shuttle service. John F. Kennedy International Airport (JFK) is 10 miles away and can be reached within 30 minutes by taxi. The hotel is situated in a vibrant Asian district that offers a variety of Eastern cuisine, as well as many stores and shops. Sponsor The conference is sponsored by the Association for Logic Programming (ALP), LogicBlox Inc., Semantic Systems, and UT Dallas. Financial Assistance The Association for Logic Programming has funds to assist financially disad vantaged participants and, especially, students to enable them to attend the conference. Inquiries should be made to the general chairs. 
From: Nils Muellner <nils.muellner@md...>  20160901 11:33:17

[Please accept our apologies if you receive multiple copies of this Call for Participation] ==================================================== CALL FOR PARTICIPATION SETTA 2016 2nd Symposium on Dependable Software Engineering Theories, Tools and Applications Beijing, China, Nov. 911, 2016 http://lcs.ios.ac.cn/setta/ ==================================================== === Important dates === Early registration deadline: October 10, 2016 Conference: Nov. 911, 2016 === Objectives and scope === The aim of the symposium is to bring together international researchers and practitioners in the field of software technology. Its focus is on formal methods and advanced software technologies, especially for engineering complex, largescale artifacts like cyberphysical systems, networks of things, enterprise systems, or cloudbased services. Contributions relating to formal methods or integrating them with software engineering, as well as papers advancing scalability or widening the scope of rigorous methods to new design goals are especially welcome. Being hosted in China, the symposium will also provide a platform for building up research collaborations between the rapidly growing Chinese computer science community and its international counterpart. The symposium will support this process through dedicated events and therefore welcomes both young researchers considering international collaboration in formal methods and established researchers looking for international cooperation and willing to attract new colleagues to the domain. Areas of interest include but are not limited to: * Requirements specification and analysis * Formalisms for modeling, design and implementation * Model checking, theorem proving, and decision procedures * Scalable approaches to formal system analysis * Formal approaches to simulation and testing * Integration of formal methods into software engineering practice * Contractbased engineering of components, systems, and systems of systems * Formal and engineering aspects of software evolution and maintenance * Parallel and multicore programming * Embedded, realtime, hybrid, and cyberphysical systems * Mixedcritical applications and systems * Formal aspects of serviceoriented and cloud computing * Safety, reliability, robustness, and faulttolerance * Empirical analysis techniques and integration with formal methods * Applications and industrial experience reports * Tool integration === Invited speakers === * Prof. Edward A. Lee (University of California at Berkeley, USA) : Dependable CyberPhysical Systems * Prof. Sriram Sankaranarayanan(University of Colorado Boulder, USA ) : From finitely many simulations to flowpipes * Prof. Mingsheng Ying (University of Technology Sydney, Australia and Tsinghua University, China) : Toward Automatic Verification of Quantum Programs === Colocated Events === SETTA 2016 will be accompanied by two colocated events: 2nd Young Researchers Workshop on Formal Methods (YRSETTA 2016) http://lcs.ios.ac.cn/setta/yrsetta/ FMAC 2016 (in Chinese) http://lcs.ios.ac.cn/setta/fmac2016/ === Conference location === SETTA 2016 is hosted by the Institute of Software, Chinese Academy of Science; the conference will take place in Building 5. 
From: Guy Katz <guyk@st...>  20160825 20:35:53

(Apologies if you receive multiple copies of this message)  NFM 2017  Call For Papers The 9th NASA Formal Methods Symposium  http://ti.arc.nasa.gov/events/nfm2017/ May 16  18, 2017 NASA Ames Research Center Moffett Field, CA, USA Theme of the Symposium  The widespread use and increasing complexity of missioncritical and safetycritical systems at NASA and in the aerospace industry require advanced techniques that address these systems’ specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM’s goals are to identify challenges and to provide solutions for achieving assurance for such critical systems. New developments and emerging applications like autonomous software for Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced separation assurance algorithms for aircraft, and the need for systemwide fault detection, diagnosis, and prognostics provide new challenges for system specification, development, and verification approaches. Similar challenges need to be addressed during development and deployment of onboard software for spacecraft ranging from small and inexpensive CubeSat systems to manned spacecraft like Orion, as well as for ground systems. The focus of the symposium will be on formal techniques and other approaches for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASArelevant safetycritical systems during all stages of the software lifecycle. Topics of interest include but are not limited to:  * Model checking * Theorem proving * SAT and SMT solving * Symbolic execution * Static analysis * Modelbased development * Runtime verification * Software and system testing * Safety assurance * Fault tolerance * Compositional verification * Security and intrusion detection * Design for verification and correctbydesign techniques * Techniques for scaling formal methods * Formal methods for multicore, GPUbased implementations * Applications of formal methods in the development of: * autonomous systems * safetycritical artificial intelligence systems * cyberphysical, embedded, and hybrid systems * faultdetection, diagnostics, and prognostics systems * Use of formal methods in: * assurance cases * humanmachine interaction analysis * requirements generation, specification, and validation * automated testing and verification Important Dates  Abstract Submission: November 28, 2016 Paper Submission: December 5, 2016 Paper notification: February 3, 2017 Camera Ready Deadline: March 1, 2017 Symposium: May 1618, 2017 Location  The symposium will take place at NASA Ames Research Center, Moffett Field, CA, USA. Registration is required but is free of charge. Submission Details  There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (maximum 15 pages) 2. Short papers on tools, experience reports, or work in progress with preliminary results (maximum 6 pages) All papers must be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by at least three members of the Program Committee. Papers will appear in a volume of Springer's Lecture Notes in Computer Science (LNCS), and must use LNCS style formatting. Papers must be submitted in PDF format at the EasyChair submission site: https://easychair.org/conferences/?conf=nfm2017 Authors of selected best papers may be invited to submit an extended version to a special issue of the Journal of Automated Reasoning (Springer). Organizing Committee   Misty Davies, NASA Ames (General Chair)  Temesghen Kahsai, NASA Ames / CMU (PC Chair)  Clark Barrett, Stanford University (PC Chair)  Guy Katz, Stanford University (Local arrangements) Program Committee   Aarti Gupta (Princeton University)  Alberto Griggio (FBKIRST)  Alessandro Cimatti (FBKIRST)  Alwyn Goodloe (NASA Langley)  Arie Gurfinkel (CMU/SEI)  Cesare Tinelli (University of Iowa)  Christoph Torens (German Aerospace Center)  Daniel Kroening (University of Oxford)  Dino Distefano (Facebook)  Dirk Beyer (LMU Munich)  Domagoj Babic (Google)  Ella Atkins (University of Michigan)  Eric Feron (Georgia Tech)  Ewen Denney (SGT / NASA Ames)  Gerwin Klein (NICTA and UNSW)  John Harrison (Intel)  John Rushby (SRI)  Jorge Navas (SGT / NASA Ames)  Julia Badger (NASA)  Kalou Cabrera Castillos (LIFC)  Kelly Hayhurst (NASA)  Kirstie L. Bellman (The Aerospace Corporation)  Klaus Havelund (NASA JPL)  Kristin Yvonne Rozier (Iowa State University)  Lael Rudd (Draper)  Lee Pike (Galois)  Martin Schäf (SRI)  Mats Heimdahl (University of Minnesota)  Meeko Oishi (University of New Mexico)  Mike Hinchey (Lerothe Irish Software Engineering Research Centre)  Michael Lowry (NASA Ames)  Murali Rangarajan (Boeing)  Natasha Neogi (NASA Langley)  Neha Rungta (SGT / NASA Ames)  Nikolaj Bjørner (Microsoft Research)  Patrice Godefroid (Microsoft Research)  Philipp Rümmer (Uppsala University)  PierreLoïc Garoche (ONERA)  Rajeev Joshi (NASA JPL)  Sriram Sankaranarayanan (University of Colorado Boulder)  Susmit Jha (United Technologies)  Virginie Wiels (ONERA)  Wenchao Li (Boston University)  Zvonimir Rakamaric (University of Utah) Steering Committee   Julia Badger, NASA Johnson Space Center, USA  Ben Di Vito, NASA Langley Research Center, USA  Klaus Havelund, NASA Jet Propulsion Laboratory, USA  Gerard Holzmann, NASA Jet Propulsion Laboratory, USA  Michael Lowry, NASA Ames Research Center, USA  Kristin Yvonne Rozier, University of Cincinnati, USA  Johann Schumann, SGT, Inc./NASA Ames Research Center, USA 
From: Andrea Rosa <andrea.rosa@us...>  20160819 07:53:36

ICPE 2017 8th ACM/SPEC International Conference on Performance Engineering Sponsored by ACM SIGMETRICS, SIGSOFT, and SPEC RG L'Aquila, Italy April 2226, 2017 https://icpe2017.spec.org/  IMPORTANT DATES Research and Industrial / Experience Abstracts: Sep 23, 2016 Research and Industrial / Experience Papers: Sep 30, 2016 Research and Industrial / Experience Paper Notification: Nov 18, 2016 WorkinProgress/Vision Papers: Nov 25, 2016 Workshop Proposals: Nov 05, 2016 Workshop Proposal Notification: Nov 19, 2016 Dates for tutorials, posters and demos will be announced.  SCOPE AND TOPICS The goal of the International Conference on Performance Engineering (ICPE) is to integrate theory and practice in the field of performance engineering by providing a forum for sharing ideas and experiences between industry and academia. Nowadays, complex systems of all types, like Webbased systems, data centers and cloud infrastructures, social networks, peertopeer, mobile and wireless systems, cyberphysical systems, the Internet of Things, realtime and embedded systems, have increasingly distributed and dynamic system architectures that provide high flexibility, however, also increase the complexity of managing endtoend application performance. ICPE brings together researchers and industry practitioners to share and present their experiences, discuss challenges, and report stateoftheart and inprogress research on performance engineering of software and systems, including performance measurement, modeling, benchmark design, and runtime performance management. The focus is both on classical metrics such as response time, throughput, resource utilization, and (energy) efficiency, as well as on the relationship of such metrics to other system properties including but not limited to scalability, elasticity, availability, reliability, and security. This year's main theme is costeffective performance engineering, where cost has a wide interpretation including measures such as effort and energy in addition to traditional performance measures. Topics of interest include, but are not limited to: Performance modeling of software * Languages and ontologies * Methods and tools * Relationship/integration/tradeoffs with other QoS attributes * Analytical, simulation and statistical modeling methodologies * Model validation and calibration techniques * Automatic model extraction * Performance modeling and analysis tools Performance and software development processes/paradigms * Software performance patterns and antipatterns * Software/performance tool interoperability (models and data interchange formats) * Performanceoriented design, implementation and configuration management * Software Performance Engineering and ModelDriven Development * Gathering, interpreting and exploiting software performance annotations and data * System sizing and capacity planning techniques * (Modeldriven) Performance requirements engineering * Relationship between performance and architecture * Collaboration of development and operation (DevOps) for performance * Performance and agile methods * Performance in ServiceOriented Architectures (SOA) * Performance of microservice architectures and containers Performance measurement, monitoring and analysis * Performance measurement and monitoring techniques * Analysis of measured application performance data * Application tracing and profiling * Workload characterization techniques * Experimental design * Tools for performance testing, measurement, profiling and tuning Benchmarking * Performance metrics and benchmark suites * Benchmarking methodologies * Development of parameterizable, flexible benchmarks * Benchmark workloads and scenarios * Use of benchmarks in industry and academia Runtime performance management * Use of models at runtime * Online performance prediction * Autonomic resource management * Utilitybased optimization * Capacity management Power and performance, energy efficiency * Power consumption models and management techniques * Tradeoffs between performance and energy efficiency * Performancedriven resource and power management Performance modeling and evaluation in different environments and application domains * Webbased systems, ebusiness, Web services * Big data systems, data analytics systems, and other data analysis systems * Internet of Things * Social networks * Cyberphysical systems * Industrial Internet (Industry 4.0) * Virtualization and cloud computing * Autonomous/adaptive systems * Transactionoriented systems * Communication networks * Parallel and distributed systems * Embedded systems * Multicore systems * Cluster and grid computing environments * High performance computing * Eventbased systems * Realtime and multimedia systems * Peertopeer, mobile and wireless systems All other topics related to performance of software and systems.  SUBMISSION GUIDELINES Authors are invited to submit original, unpublished papers that are not being considered in another forum. A variety of contribution styles for papers are solicited including: basic and applied research papers for novel scientific insights, industrial and experience papers reporting on applying performance engineering or benchmarks in practice, and workinprogress/vision papers for ongoing but yet interesting work. Different acceptance criteria apply based on the expected content of the individual contribution types. Authors will be requested to selfclassify their papers according to topic and contribution style when submitting their papers. Submissions to all tracks need to be uploaded to ICPE's submission system and conform to the ACM submission format. For detailed submission instructions, please visit: https://icpe2017.spec.org/submissions.html. At least one author of each accepted paper is required to register at the full rate, attend the conference and present the paper. Presented papers will be published in the ICPE 2017 conference proceedings that will be published by ACM and included in the ACM Digital Library. After the conference, there will be a call for a special issue of a journal. AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.)  PROGRAM COMMITTEE (RESEARCH PAPERS) Amy Apon, Clemson University Martin Arlitt, HP Labs and University of Calgary Alberto Avritzer, Performance Engineering Consultant Steffen Becker, University of Technology Chemnitz Robert Birke, IBM Zurich Research Laboratory Andre B. Bondi, Software Performance and Scalability Consulting LLC Niklas Carlsson, Linkoping University Lydia Y. Chen, IBM Zurich Research Laboratory Lucy Cherkasova, HP Labs Antinisca Di Marco, Università dell'Aquila Wilhelm Hasselbring, Kiel University Alexandru Iosup, Delft University of Technology Evangelia Kalyvianaki, City University London Samuel Kounev, University of Wuerzburg Heiko Koziolek, ABB Corporate Research Diwakar Krishnamurthy, University of Calgary Patrick Lee, The Chinese University of Hong Kong Catalina M. Lladó, Universitat Illes Balears Lei Lu, VMware Andrea Marin, University of Venice Daniel Menasce, George Mason University Daniel S. Menasché, Federal Univ. of Rio de Janeiro José Merseguer, Universidad de Zaragoza Ningfang Mi, Northeastern University Raffaela Mirandola, Politecnico di Milano Manoj Nambiar, Tata Consultancy Services Dorina Petriu, Carleton University Denys Poshyvanyk, College of William and Mary Ralf Reussner, Karlsruhe Institute of Technology Alma Riska, Network Appliances Jerry Rolia, HP Labs Rekha Singhal, Tata Consultancy Services Mirco Tribastone, IMT Institute for Advanced Studies Catia Trubiani, Gran Sasso Science Institute Petr Tuma, Charles University Ana Lucia Varbanescu, University of Amsterdam Enrico Vicario, University of Florence Katinka Wolter, Freie Universitaet zu Berlin Murray Woodside, Carleton University Feng Yan, University of NevadaReno Xiaoyun Zhu, Futurewei Technologies Inc  ORGANIZING COMMITTEE General Chairs * Walter Binder, Università della Svizzera italiana (USI), Switzerland * Vittorio Cortellessa, Università dell'Aquila, Italy Research Program Chairs * Anne Koziolek, Karlsruhe Institute of Technology, Germany * Evgenia Smirni, College of William and Mary, USA Industry Program Chairs * Meikel Poess, Oracle, USA Tutorials Chair * Valeria Cardellini, Università di Roma Torvergata, Italy Workshops Chairs * Hanspeter Mössenböck, Johannes Kepler Universität Linz, Austria * Catia Trubiani, Gran Sasso Science Institute, Italy Posters and Demos Chair * Lubomir Bulej, Charles University, Czech Republic Awards Chairs * Petr Tuma, Charles University, Czech Republic * Murray Woodside, Carleton University, Canada Local Organization Chair * Antinisca Di Marco, Università dell'Aquila, Italy Publicity Chairs * Andrea Rosà, Università della Svizzera italiana (USI), Switzerland * Diego Perez, Politecnico di Milano, Italy Finance Chair * André van Hoorn, University of Stuttgart Publication and Registration Chair * Davide Arcelli, Università dell'Aquila, Italy Web Site Chair * Cathy Sandifer, SPEC, USA  Andrea Rosà PhD student  Teaching assistant Faculty of Informatics  2nd floor Università della Svizzera italiana (USI) Via G. Buffi 13 CH6904 Lugano Switzerland (e) andrea.rosa@...<mailto:andrea.rosa@...> (p) +41 58 666 4455 ext. 2183 (w) http://www.inf.usi.ch/phd/rosaa/ 
From: Thomas Melham <thomas.melham@ba...>  20160818 21:44:41

The book is indeed of mainly historical interest now. I suppose we could ask CUP for permission to put it into the public domain. It is long out of print, I believe. Tom > On 18 Aug 2016, at 17:03, Ken Kubota <mail@...> wrote: > > 1. If the print proof file for the HOL book from 1993 is still available, it > could be converted to PDF format and made part of the CL technical report > series, such that it would be available online (even if only for historical > interest). 
From: Peter Schueller <peter.schuller@ma...>  20160818 19:15:06

(Apologies if you receive multiple copies of this email. Please distribute to interested parties.) Call For Participation 32nd International Conference on Logic Programming New York City, USA October 1621, 2016 http://software.imdea.org/Conferences/ICLP2016/ News:  The list of accepted papers is available online: http://software.imdea.org/Conferences/ICLP2016/accepted.html  Early registration deadline: September 5.  Invited talks: * Arun Majumdar: One Billion Dollars, Global Warming and Logic Programming. * Francesca Rossi: Embedding Ethical Principles in Decision Support Systems: Can (Constraint) Logic Programming Play a Role?  Tutorials: * Michael Kifer, Theresa Swift and Benjamin Grosof: Practical Knowledge Representation and Reasoning in Ergo. * Yuliya Lierler: Relating Constraint Answer Set Programming and Satisfiability Modulo Theories.  Autumn School on Computational Logic: http://iclp16school.webs.upv.es/ * Roman Bartak: Constraint Logic Programming * Veronica Dahl: Language processing through logic grammars and constraints * Torsten Schaub: Answer Set Programming: foundations and applications * C.R.Ramakrishnan: Verification and probabilistic logic programming  Sponsors: * The Association for Logic Programming: http://logicprogramming.org/ * LogicBlox, Inc: http://www.logicblox.com/ * Semantic Systems: http://www.semanticsystems.com/ * UT Dallas: http://www.utdallas.edu/ Conference Scope Since the first conference held in Marseille in 1982, ICLP has been the pre mier international conference for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to:  Theory: Semantic Foundations, Formalisms, Nonmonotonic Reasoning, Knowledge Representation.  Implementation: Compilation, Virtual Machines, Parallelism, Constraint Han dling Rules, Tabling.  Environments: Program Analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing.  Language Issues: Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, Programming Techniques.  Related Paradigms: Inductive and Coinductive Logic Programming, Constraint Logic Programming, AnswerSet Programming, SATChecking.  Applications: Databases, Big Data, Data Integration and Federation, Soft ware Engineering, Natural Language Processing, Web and Semantic Web, Agents, Artificial Intelligence, Bioinformatics, and Education. In addition to the presentations of accepted papers, the technical program will include invited talks, advanced tutorials, the doctoral consortium, and several workshops. Important Dates Early Registration Deadline: September 5, 2016 Conference: October 1621, 2016 Conference Organization General Chairs: Michael Kifer Stony Brook University, USA NengFa Zhou City University of New York, USA Program Chairs: Manuel Carro UPM and IMDEA Software Institute, Spain Andy King University of Kent, UK Workshop Chair: Marcello Balduccini Drexel University, USA Publicity Chair: Peter Schueller Marmara University, Turkey Doctoral Consortium Chairs: Marina De Vos University of Bath, UK Neda Saeedloei University of Minnesota Duluth, USA Programming Contest Chair: Paul Fodor Stony Brook University, USA Web Presence: Joaquin Arias IMDEA Software Institute, Spain Program Committee: Marcello Balduccini Drexel University, USA Mutsunori Banbara Kobe University, Japan Roman Bartak Charles University, Czech Republic Pedro Cabalar University of Corunna, Spain Mats Carlsson SICS, Sweden Manuel Carro UPM and IMDEA Software Institute, Spain Michael Codish BenGurion University of the Negev, Israel Marina De Vos University of Bath, UK Agostino Dovier Universita degli Studi di Udine, Italy Gregory Duck National University of Singapore, Singapore Esra Erdem Sabanci University, Turkey Wolfgang Faber University of Huddersfield, UK Thom Fruehwirth University of Ulm, Germany John Gallagher Roskilde University, Denmark, and IMDEA Software Institute, Spain Marco Gavanelli Universita degli Studi di Ferrara, Italy Martin Gebser University of Potsdam, Germany Michael Hanus CAU Kiel, Germany Katsumi Inoue NII, Japan Gerda Janssens KU Leuven  University of Leuven, Belgium Andy King University of Kent, UK Ekaterina Komendantskaya HeriotWatt University, UK Michael Leuschel University of Dusseldorf, Germany Vladimir Lifschitz University of Texas, USA Jose F. Morales IMDEA Software Institute, Spain Enrico Pontelli New Mexico State University, USA Jorg Puhrer Leipzig University, Germany Ricardo Rocha University of Porto, Portugal Zoltan Somogyi Independent Researcher, Australia Harald Sondergaard University of Melbourne, Australia Theresa Swift NOVALINKS, US, and UNL, Portugal Francesca Toni Imperial College London, UK Irina Trubitsyna University of Calabria, Italy Mirek Truszczynski University of Kentucky, USA Alicia Villanueva Universitat Politecnica de Valencia, Spain Jan Wielemaker VU University Amsterdam, Netherlands Stefan Woltran TU Wien, Austria Fangkai Yang Schlumberger Inc., USA JiaHuai You University of Alberta, Canada Workshops The ICLP 2016 program will include several workshops. They are perhaps the best places for the presentation of preliminary work, underdeveloped novel ideas, and new open problems to a wide and interested audience with opportuni ties for intensive discussions and project collaboration. Autumn School on Computational Logic Students and researchers are invited to participate in the Autumn School with the following tutorials: * Roman Bartak: Constraint Logic Programming * Veronica Dahl: Language processing through logic grammars and constraints * Torsten Schaub: Answer Set Programming: foundations and applications * C.R.Ramakrishnan: Verification and probabilistic logic programming Information on scholarships can be found on the homepage: http://iclp16school.webs.upv.es/ Doctoral Consortium The Twelfth Doctoral Consortium (DC) on Logic Programming provides research students with the opportunity to present and discuss their research direc tions, and to obtain feedback from both peers and experts in the field. Accepted participants will receive partial financial support to attend the event and the main conference. The best paper from the DC will be given the opportunity to present in a session of the main ICLP conference. Conference Venue The venue will be the Sheraton LaGuardia East Hotel in Flushing, New York City. New York City is an international tourist destination, receiving 56 million tourists in 2014 alone. Several sources have ranked New York the most photographed city in the world. Times square, known as the city's heart, is the brightly illuminated hub of the Broadway theatre district. The Statue of Liberty greets new arrivals to the Americas by ship in the late 19th and early 20th century, and is a globally recognized symbol of the United States. Flush ing is associated by many with the National Tennis Centre, since Flushing Meadows has been the home of the US Open Grand Slam tennis tournament every year since 1978. New York is the most populous city in the United States and one of the most populous urban agglomerations in the world. Situated in one of the world's largest natural harbours, New York City consists of five boroughs, each of which is a separate county of New York State. The conference hotel is situated in the Queens borough, just a twominute walk from the FlushingMain Street rail station. Direct train lines take you directly from there to Times Square in just over 45 minutes, which is fast for New York City. The Museum of Modern Art can be reached in under 40 mins, Grand Central Terminal in 40 mins, the Empire State Building under 50 mins, and The High Line Park in 50 minutes. The hotel is also close to LaGuardia Airports and JFK. LaGuardia is just 3 miles away and the hotel offers a complementary shuttle service. John F. Kennedy International Airport (JFK) is 10 miles away and can be reached within 30 minutes by taxi. The hotel is situated in a vibrant Asian district that offers a variety of Eastern cuisine, as well as many stores and shops. Sponsor The conference is sponsored by the Association for Logic Programming (ALP), LogicBlox Inc., Semantic Systems, and UT Dallas. Financial Assistance The Association for Logic Programming has funds to assist financially disad vantaged participants and, especially, students to enable them to attend the conference. Inquiries should be made to the general chairs. 
From: Ken Kubota <mail@ke...>  20160818 16:03:28

Dear Members of the Research Community, The question raised in section 2 of my email available online at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00069.html has now been answered, as the quote already appears in the HOL book from 1993, which I was able to get hold of today: "From a logical point of view, it would be better to have a simpler substitution primitive, such as 'Rule R' of Andrews' logic Q0, and then to derive more complex rules from it." [Gordon/Melham, 1993, p. 213] The author of this quote in Part III (pp. 191232) is Andrew M. Pitts: "Part III presents the logic supported by HOL ('The HOL Logic'). It consists of two chapters: an informal introduction and a formal settheoretic semantics (written by Andrew Pitts)." [Gordon/Melham, 1993, p. xv] In addition to Pitts' insight, the use of the description operator (like in Andrews' Q0) should be preferred to the use of the epsilon operator (used by Gordon, who already called it "suspicious"), as discussed in section 3 of my email available online at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00069.html Whereas the reducibility of rules cannot be preserved when featuring automation instead of expressiveness, as one has to switch from a Hilbertstyle system to natural deduction, the reducibility of symbols and variable binders remains, and unnecessary use of axioms like the Axiom of Choice should be avoided. For the HOL documentation team, I have two suggestions. 1. If the print proof file for the HOL book from 1993 is still available, it could be converted to PDF format and made part of the CL technical report series, such that it would be available online (even if only for historical interest). 2. Restoring the original quote would be preferable, as there is a comma missing in the current HOL4 document: "From a logical point of view it would be better to have a simpler substitution primitive, such as 'Rule R' of Andrews' logic Q0, and then to derive more complex rules from it." http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf (p. 27) Kind regards, Ken Kubota References Gordon, Michael J. C., and Melham, Thomas F., eds. (1993), Introduction to HOL: A theorem proving environment for higher order logic, Cambridge: Cambridge University Press. ISBN 0521441897. ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 
From: Lawrence Paulson <lp15@ca...>  20160817 14:40:54

CALL FOR PAPERS Special Issue On MILESTONES IN INTERACTIVE THEOREM PROVING Journal of Automated Reasoning The past few decades have seen major achievements in interactive theorem proving, such as the formalisation of deep mathematical theorems and significant bodies of theoretical computer science, as well as the verification of complex software and hardware systems. Too often, these impressive results have been published in abbreviated or fragmentary form in conference proceedings, or not at all. This special issue welcomes fulllength papers describing past work not previously published in a journal, along with new developments of any length. Small, selfcontained Proof Pearls and applications of all kinds are also welcome. This special issue will be devoted to applications of interactive theorem proving in their full variety: formalised mathematics, formalised theory, formalised semantics, formal proofs of hardware or software systems. They can be large or small. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. Papers should be in pdf format, following the JAR guidelines for authors, and be submitted using the usual Springer online submission system: http://www.editorialmanager.com/jars/default.aspx When you reach the dropdown menu "Choose Article Type", you must select "S.I. : MILESTONE" to specify the special issue.. To encourage a speedy review cycle, it will be expected that authors of submissions also serve as referees. Important Dates 1 Apr 2017 Submission Deadline 1 Oct 2017 Notification of accepted papers 1 Jan 2018 Final version For more information, please see http://www.cse.unsw.edu.au/~kleing/JARmilestone/ Guest Editors Larry Paulson, University of Cambridge Jeremy Avigad, Carnegie Mellon University Gerwin Klein, Data61 and UNSW Australia 
From: Ken Kubota <mail@ke...>  20160815 15:53:59

Dear Members of the Research Community, Please allow me to add a few comments. 1. First, I would like to thank Larry Paulson for providing the download link for Mike Gordon's text at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00047.html answering my inquiry at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00046.html What Gordon calls "'second order' [lambda]terms like \a. \x:a. x, [which] perhaps [...] should be included in the HOL logic" at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 22) is implemented in R0 as the main feature of dependent type theory (i.e., the binding of type variables with lambda) and called "type abstraction" there: http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (pp. 356 ff.) It might be worth considering publishing this 2001 version of Gordon's paper within the technical report series in order to ensure longterm (online) availability of the currently only cached document. In addition, online availability of the 1985 version (UCAMCLTR68) is desirable, as it is still of historical interest. Also, I would like to thank Tom Melham for bringing to my attention his approach of implementing in the HOL logic the idea of explicit quantification over type variables as presented by Andrews in 1965: "I have found Andrews' book [1] invaluable in working out many of the technical details of the extension to HOL proposed here." http://www.cs.ox.ac.uk/tom.melham/pub/Melham1994HLE.pdf (p. 15) I have addressed this issue and discussed details in my draft: "It has to be noted that already in his PhD thesis 'A Transfinite Type Theory with Type Variables' published in 1965 Andrews is very near to developing a dependent type theory. [...] In the system Q with type variables the universal quantifier (∀) becomes a true variable binder in the case of types, but in the case of terms (objects) a definition depending on λ." [Kubota, 2015, p. 31] However, for some reason Andrews refrained from directly using lambda as type variable binder, which would exhibit the reducibility of the variable binders to a single one, as was done in R0. 2. In the LOGIC part of the documentation of the current HOL system, reference is made to Rule R of Andrews' logic Q0: "From a logical point of view it would be better to have a simpler substitution primitive, such as 'Rule R' of Andrews' logic Q0, and then to derive more complex rules from it." http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf (p. 27) Is it possible to figure out the author of this sentence? I am considering quoting it and would like to credit authorship in such a case. 3. Preferring definitions over the use of nonlogical axioms as discussed at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016August/msg00046.html has a major advantage to be mentioned. If the conditions are not introduced as axioms, but as properties within the definition, and these conditions later turn out to be contradictory, they do not render the system inconsistent as a whole, but only demonstrate that no mathematical object ("model") can satisfy these conditions, which is formally expressed by the emptiness of the defined set, which is the desired result (in the simplest case concerning the types, i.e., a unary predicate; otherwise tuples may be used). For this reason, and for other reasons, such as not constraining expressiveness of the system, instead of postulating a (nonlogical) Axiom of Infinity (usually over the type of individuals), the Peano axioms should be part of the definition of natural numbers (which can be expressed without axioms quite simply and naturally in dependent type theory), that guarantees the set to be infinite: "Actually, any set satisfying postulates P1P4 must be infinite." [Andrews, 2002, p. 259] Then there is no need to add an Axiom of Infinity as Axiom 6, which extends Q0 to Q0^inf [cf. Andrews, 2002, p. 259]. For the same reasons, the use of language elements which make implicit use of axioms should be avoided. Gordon correctly states: "The inclusion of [epsilon]terms into HOL 'builds in' the Axiom of Choice [...]." Somewhat earlier on the same page, he quite frankly confesses: "It must be admitted that the [epsilon]operator looks rather suspicious." http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 24) Implicit use of the Axiom of Choice can be avoided by using the description operator instead, like in Q0 and R0, where it is the counterpart to identity (equality) [cf. Andrews, 2002, pp. 211, 213; Kubota, 2015]. For example, the "conditional term Cond t t_1 t_2 (meaning 'if t then t_1 else t_2')" "defined using the [epsilon]operator" at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 24) can be defined using the description operator [cf. Andrews, 2002, pp. 235 f. (5313)]; software verification of the formal proof has been provided in [Kubota, 2015, pp. 165174]. The (verification of the) formal proof and the axioms for R0 have now been made available online at: http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf Please note that in Axiom 5 (Axiom of Descriptions) and throughout the whole system the primitive symbol for identity (equality) 'Q' used in Q0 [cf. Andrews, 2002, pp. 211, 213] was eliminated and replaced by the identity symbol '=' in R0, as the symbol 'Q' syntactically doesn't have an own independent function: http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (pp. 351 f.) It then becomes even more obvious that description is the counterpart to identity, extracting the single element from a singleton (unit set), and eliminating the identity symbol '='. 4. Rule R is indeed presented by Andrews as the "single rule of inference" [Andrews, 2002, p. 213] of Q0. However, already on the following page, a variant, Rule R', is specified [cf. p. 214], which also takes into account a set of hypotheses. Hence, logically, one might regard Rule R' as the general rule and Rule R only as the special case in which the set of hypotheses is empty. Technically, both Rule R and Rule R' are implemented in the dependent type theory R0 as two different routines due to the access to different parts of the formulae, but both routines then use the same subroutine. Rule R and Rule R' are called §s and §s' in R0, where the section sign (§) indicates a rule, and 's' stands for substitution: http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (pp. 362 f.) Rule §\ ('\' stands for lambda) denotes lambdaconversion (or more specifically, betaconversion), which in Andrews' Q0 is obtained as theorem 5207 [cf. Andrews, 2002, p. 218 f.] from Axiom Schemata 4_1  4_5. Since some of the Axiom Schemata 4_1  4_5 contain restrictions, lambdaconversion was implemented as a rule in R0. As the active elements, rules may contain restrictions, but not theorems (including axioms/axiom schemata), which are passive elements. This alternative method of implementing lambdaconversion was already considered by Andrews in a paragraph to which he directed my attention when I met him and which is already contained in the first edition (1986): "5207 could be taken as an axiom schema in place of 4_1  4_5, and for some purposes this would be desirable, since 5207 has a conceptual simplicity and unity which is not apparent in 4_1  4_5." [Andrews, 1986, p. 165; Andrews, 2002, p. 214] The fact that lambdaconversion is actually a process (i.e., active, dynamic, and hence, a rule), and not only a (passive, static) theorem, axiom, or axiom schema, becomes obvious in the online presentation of Q0, where Axiom Schemata 4_1  4_5 are replaced by 5207 as new Axiom Schema 4 which makes use of a function "SubFree" denoting the process of substitution (of all free occurrences of a variable): http://plato.stanford.edu/archives/spr2014/entries/typetheorychurch/#ForBasEqu Similarly, in Church's simple theory of types, lambdaconversion (betaconversion) is implemented as the second (betareduction, also called betacontraction) and third (betaexpansion) of altogether six rules of inference [cf. Church, 1940, p. 60]. Kind regards, Ken Kubota References Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0120585359 (Hardcover). ISBN 0120585367 (Paperback). Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: Kluwer Academic Publishers. ISBN 1402007639. DOI: 10.1007/9789401599344. Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/archives/spr2014/entries/typetheorychurch/ (July 2, 2016). Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: Journal of Symbolic Logic 5, pp. 5668. Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, 2015). Unpublished manuscript. SHA512: a0dfe205eb1a2cb29efaa579d68fa2e5 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: http://dx.doi.org/10.4444/100.10 Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (p. 1, pp. 356364, pp. 411420, and pp. 754755). Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (January 24, 2016). SHA512: 67a48ee12a61583bd82c286136459c0c 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 3d1047d1831bc357eb57b263b44c885b. Kubota, Ken (2015b), Excerpt from [Kubota, 2015] (p. 1, pp. 165174, and pp. 350352). Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (August 13, 2016). SHA512: 8702d932d50f2e1f6b592dc03b6f283e 64ba18f881150b4ae32e4b915249d241 3db34ba4c3dcf0e0cdef25b679d9615f 424adb1803a179e578087ded31b573b9. ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 
From: Pedro López García <pedro.lopez@im...>  20160815 09:41:11

============================================================ LAST CALL FOR PARTICIPATION: LOPSTR 2016 26th International Symposium on LogicBased Program Synthesis and Transformation, Edinburgh, Scotland UK, September 68, 2016 http://www.cliplab.org/Conferences/LOPSTR16/ colocated with PPDP 2016 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, Scotland UK, September 57, 2016 http://ppdp16.webs.upv.es/ and SAS 2016 23rd Static Analysis Symposium, Edinburgh, Scotland UK, September 810, 2016 http://staticanalysis.org/sas2016/ ============================================================ Registration is open at: http://conferences.inf.ed.ac.uk/ppdplopstrsas2016/ ** EARLY REGISTRATION UNTIL AUGUST 15 ** VISA Please check here: https://www.gov.uk/checkukvisa whether you require a visa to visit the UK. If so, contact us as soon as possible as explained here: http://conferences.inf.ed.ac.uk/ppdplopstrsas2016/registration.html Getting a visa can take from 36 weeks depending on the nationality and country from which applying. We recommend that anyone considering attending who needs a visa register now and apply now. If you are eventually unable to attend due to visa issues we will refund your registration fee. INVITED TALKS  Greg Morrisett, Cornell University, USA (jointly with PPDP'16): Challenges in Compiling Coq.  Francesco Logozzo, Facebook, USA (jointly with PPDP'16): Abstract interpretation for taint analysis at scale.  Martin Vechev, ETH Zurich, Switzerland (jointly with SAS'16): Learning from Programs: Probabilistic Models, Program Analysis and Synthesis. ACCEPTED PAPERS  Symbolic Abstract Contract Synthesis in a Rewriting Framework. María Alpuente, Daniel Pardo and Alicia Villanueva.  Coinductive Soundness of Corecursive Type Class Resolution. Frantisek Farka, Ekaterina Komendantskaya, Kevin Hammond and Peng Fu.  MiniZinc with Strings. Roberto Amadini, Pierre Flener, Justin Pearson, Joseph D. Scott, Peter J. Stuckey and Guido Tack.  On the Completeness of Selective Unification in Concolic Testing of Logic Programs. Fred Mesnard, Etienne Payet and German Vidal.  Verification of TimeAware Business Processes using Constrained Horn Clauses. Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo, Alberto Pettorossi and Maurizio Proietti.  Tuning Fuzzy Logic Programs with Symbolic Execution. Gines Moreno, Jaime Penabad and German Vidal.  A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed SimplyTyped Lambda Terms and Normal Forms. Paul Tarau.  A New FunctionalLogic Compiler for Curry: Sprite. Sergio Antoy and Andy Jost.  Towards Reversible Computation in Erlang. Naoki Nishida, Adrian Palacios and German Vidal.  Slicing Concurrent Constraint Programs. Moreno Falaschi, Maurizio Gabbrielli, Carlos Olarte and Catuscia Palamidessi.  Scaling Bounded Model Checking By Transforming Programs With Arrays. Anushri Jana, Uday Khedker, Advaita Datar, R Venkatesh and Niyas C.  Hierarchical Shape Abstraction of FreeList Memory Allocators. Bin Fang and Mihaela Sighireanu.  A Productivity Checker for Logic Programming. Ekaterina Komendantskaya, Patricia Johann and Martin Möhrmann.  Automata Theory Approach to Predicate Intuitionistic Logic. Maciej Zielenkiewicz and Aleksy Schubert.  Nominal Unification of Higher Order Expressions with Recursive Let. Manfred SchmidtSchauss, Temur Kutsia, Jordi Levy and Mateu Villaret.  A Formal, Resource ConsumptionPreserving Translation of Actors to Haskell. Elvira Albert, Nikolaos Bezirgiannis, Frank De Boer and Enrique MartinMartin.  Partial Evaluation of Ordersorted Equational Programs modulo Axioms. María Alpuente, Angel Cuenca, Santiago Escobar and Jose Meseguer.  lpopt: A Rule Optimization Tool for Answer Set Programming. Manuel Bichler, Michael Morak and Stefan Woltran.  CurryCheck: Checking Properties of Curry Programs. Michael Hanus.  Intuitionistic Logic Programming for SQL. Fernando SaenzPerez. Hope to see you in Edinburgh! Manuel Hermengildo and Pedro LopezGarcia LOPSTR 2016 Cochairs 
From: <Michael.N<orrish@da...>  20160811 23:34:08

This is certainly a nice idea. If you do figure out how to do it, please make a pull request. In work that I haven’t polished or committed, I have generalized our graph generation to target arbitrary theory hierarchies, and this generates theory summaries of its own. If that’s all you want, I can try to make it commitable. (The fact that we have two flavours of theory presentation in our help system is a wart all on its own…) Michael On 11/08/2016, 12:45, "Corey Richardson" <corey@...> wrote: Greetings HOL developers, As a HOL newbie, getting started trying to contribute to CakeML had me looking for something like the HOL reference page[0] for its theories. I made some failed attempts trying to hack up the documentation generation tool in help/srcsml to support "arbitrary" sigobjlike directories. Has anyone done this before, or have some advice on how to enable it? Is it valuable to others? [0]: https://holtheoremprover.org/kananaskis10helpdocs/help/HOLindex.html Best,  cmr +610481782084 http://octayn.net/ 
From: Corey Richardson <corey@oc...>  20160811 02:46:08

Greetings HOL developers, As a HOL newbie, getting started trying to contribute to CakeML had me looking for something like the HOL reference page[0] for its theories. I made some failed attempts trying to hack up the documentation generation tool in help/srcsml to support "arbitrary" sigobjlike directories. Has anyone done this before, or have some advice on how to enable it? Is it valuable to others? [0]: https://holtheoremprover.org/kananaskis10helpdocs/help/HOLindex.html Best,  cmr +610481782084 http://octayn.net/ 
From: Lawrence Paulson <lp15@ca...>  20160809 10:17:29

It can be downloaded from here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6103 Larry Paulson > On 8 Aug 2016, at 12:13, Ken Kubota <mail@...> wrote: > > Dear Members of the Research Community, > > As part of my efforts to try to understand the type system of Isabelle/HOL, I > have gathered the references from the mails written by Corey Richardson and > Michael Norrish and from The Isabelle/Isar Reference Manual, especially from > a) Chapter 10: HigherOrder Logic (pp. 236 f.) > b) § 11.7 Semantic subtype definitions (pp. 260263) > c) § 11.8 Functorial structure of types (pp. 263 f.). > > In all cases, with one exception, I was able to obtain either the link to the > online version or the ISBN number. > > > The exception is Mike Gordon's text "HOL: A machine oriented formulation of > higher order logic" (Technical Report 68, University of Cambridge Computer > Laboratory), registered at > http://www.cl.cam.ac.uk/techreports/UCAMCLTR68.html > > As Isabelle is provided by the University of Cambridge Computer Laboratory, > among others, would it be possible for the Isabelle developers to make this > technical report available online as a PDF file? This was done for the first > five reports listed at > http://www.cl.cam.ac.uk/techreports/UCAMCLTRtable.html > > According to the references supplied with the traditional (Mike Gordon's) HOL > variant, a revised version exists: "Technical Report No.\ 68 (revised > version)", quoted from > https://github.com/HOLTheoremProver/HOL/blob/master/Manual/Description/references.tex > Either both versions or the revised version should be made available. > > > I would like to take this opportunity to thank Michael Norrish for his advice. > The LOGIC part of HOL4 system's documentation at > http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf > is the kind of short and precise formulation of the logical core I recently > proposed for Isabelle/HOL, too: > https://lists.cam.ac.uk/pipermail/clisabelleusers/2016July/msg00105.html > > In this HOL4 document, it is stated: "From a logical point of view it would be > better to have a simpler substitution primitive, such as 'Rule R' of Andrews' > logic Q0, and then to derive more complex rules from it." (p. 27) > This is exactly the same idea that I presented recently: "The main criterion is > expressiveness [cf. Andrews, 2002, p. 205], or, vice versa, the reducibility of > mathematics to a minimal set of primitive rules and symbols. [...] For the > philosopher it is not proof automation but expressiveness that is the main > criterion, such that the method with the least amount of rules of inferences, > i.e., a Hilbertstyle system, is preferred, and all other rules become derived > rules." > https://lists.cam.ac.uk/pipermail/clisabelleusers/2016July/msg00028.html > > Similarly, the HOL4 document argues in favor of definitions instead of > introducing new axioms: "The advantages of postulation over definition have > been likened by Bertrand Russell to the advantages of theft over honest toil. > As it is all too easy to introduce inconsistent axiomatizations, users of the > HOL system are strongly advised to resist the temptation to add axioms, but to > toil through definitional theories honestly." [p. 33] > In the same manner, I wrote: "One consequence [...] is to avoid the use of > nonlogical axioms. [...] The appropriate way to deal with objects of certain > properties is to create a set of objects with these properties." [Kubota, 2015, > p. 29] > For this reason, in the R0 implementation, the group axioms are expressed not > as axioms, but as properties in the definition of "Grp" (wff 266): > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 359) > > > Kind regards, > > Ken Kubota > > > > Sources > > [S1] The Isabelle/Isar Reference Manual (February 17, 2016) > http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isarref.pdf > > [S2] Reference in the email written by Corey Richardson > https://lists.cam.ac.uk/pipermail/clisabelleusers/2016July/msg00070.html > > Dmitry Traytel / Andrei Popescu / Jasmin C. Blanchette, Foundational, > Compositional (Co)datatypes for HigherOrder Logic: Category Theory Applied to > Theorem Proving > http://dx.doi.org/10.1109/LICS.2012.75 > https://www21.in.tum.de/~traytel/papers/lics12codatatypes/codat.pdf > > [S3] Reference in the email written by Michael Norrish > "The chapters from the HOL book mentioned above are available as part of the > HOL4 system's documentation at: > http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf/download > See §2.5.4 in particular for a discussion of how the system can be extended > with new types." > > The HOL System: LOGIC (November 6, 2014) > http://sourceforge.net/projects/hol/files/hol/kananaskis10/kananaskis10logic.pdf > > > Derived References (from [S1], pp. 260263) > > [15] W. M. Farmer. The seven virtues of simple type theory. J. Applied Logic, > 6(3):267286, 2008. > http://imps.mcmaster.ca/doc/sevenvirtues.pdf > > [18] M. J. C. Gordon. HOL: A machine oriented formulation of higher order > logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985. > > [50] A. Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors, > Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, > pages 191232. Cambridge University Press, 1993. > ISBN 0521441897 > > [57] M. Wenzel. Type classes and overloading in higherorder logic. In E. L. > Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs > '97, volume 1275 of Lecture Notes in Computer Science. SpringerVerlag, 1997. > http://www4.in.tum.de/~wenzelm/papers/axclassTPHOLs97.pdf > > [22] F. Haftmann and M. Wenzel. Constructive type classes in Isabelle. In T. > Altenkirch and C. McBride, editors, Types for Proofs and Programs, TYPES 2006, > volume 4502 of LNCS. Springer, 2007. > http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf > > [27] O. Kuncar and A. Popescu. A consistent foundation for Isabelle/HOL. In C. > Urban and X. Zhang, editors, Interactive Theorem Proving  6th International > Conference, ITP 2015, Nanjing, China, August 2427, 2015, Proceedings, volume > 9236 of Lecture Notes in Computer Science. Springer, 2015. > http://www21.in.tum.de/~kuncar/kuncarpopescujar2016.pdf > http://andreipopescu.uk/pdf/ITP2015.pdf > > > Standard References > > Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0120585359 > (Hardcover). ISBN 0120585367 (Paperback). > > Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: > Kluwer Academic Publishers. ISBN 1402007639. DOI: 10.1007/9789401599344. > > Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of > Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at > http://plato.stanford.edu/archives/spr2014/entries/typetheorychurch/ (July 2, > 2016). > > Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: > Journal of Symbolic Logic 5, pp. 5668. > > > Further References > > Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, > 2015). Unpublished manuscript. SHA512: a0dfe205eb1a2cb29efaa579d68fa2e5 > 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 > 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: > http://dx.doi.org/10.4444/100.10 > > Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356364, pp. 411420, and > pp. 754755). Available online at > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf > (January 24, 2016). SHA512: 67a48ee12a61583bd82c286136459c0c > 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 > 3d1047d1831bc357eb57b263b44c885b. > > ____________________ > > Ken Kubota > doi: 10.4444/100 > http://dx.doi.org/10.4444/100 > > 