hol-info  

Messages by Thread

• • Re: [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Michael.Norrish
  • Re: [Hol-info] How to prove this theorem about relations? Michael.Norrish
  • Re: [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Jeremy Dawson
  • Re: [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Scott Owens
  • Re: [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Michael.Norrish
• [Hol-info] DICE-FOPARA 2017: Call for Papers Georg Moser
• [Hol-info] [fm-announcements] RV'17 - First call for papers and tutorials Havelund, Klaus (348B)
• [Hol-info] SEFM 2017: Call for Workshops Marco Roveri
• [Hol-info] CADE-26 Call for Papers Geoff Sutcliffe
• [Hol-info] TABLEAUX 2017 - 2nd Call for Papers Geoff Sutcliffe
• [Hol-info] TABLEAUX 2017 - Second Call for Papers Cláudia Nalon
• [Hol-info] ACL2 2017 Submission Deadline Extension Warren A. Hunt Jr.
• [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Chun Tian (binghe)
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Chun Tian (binghe)
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Thomas Tuerk
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Konrad Slind
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Michael.Norrish
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Konrad Slind
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Michael.Norrish
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Michael.Norrish
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Chun Tian (binghe)
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Chun Tian (binghe)
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Michael.Norrish
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Makarius
  • Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Chun Tian (binghe)
• [Hol-info] [fm-announcements] SPIN 2017 in Santa Barbara, CA, USA - 1 month from the paper submission deadline Havelund, Klaus (348B)
• [Hol-info] LPAR-21 extended deadlines Geoff Sutcliffe
• [Hol-info] MFPS 33: first call for papers Alexandra Silva
• [Hol-info] First School on Foundations of Programming and Software systems -- Probabilistic programming Renato Neves
• [Hol-info] CfP: MARS 2017 - Models for Formal Analysis of Real Systems [deadline extended] Peter.Hoefner
• [Hol-info] Difficulties when migrating proof scripts from Coq Chun Tian (binghe)
  • Re: [Hol-info] Difficulties when migrating proof scripts from Coq Yong Kiam
  • Re: [Hol-info] Difficulties when migrating proof scripts from Coq Chun Tian (binghe)
  • Re: [Hol-info] Difficulties when migrating proof scripts from Coq Jeremy Dawson
  • Re: [Hol-info] Difficulties when migrating proof scripts from Coq Chun Tian (binghe)
• [Hol-info] Postdoc in SDN verification and security at Edinburgh David Aspinall
• [Hol-info] WOSP-C'17 @ ACM/SPEC ICPE'17 - Call for Papers - Deadline extended Andrea Rosa
• [Hol-info] Special issue of AI Communications on Automated Reasoning Geoff Sutcliffe
• [Hol-info] ACL2 2017 Call for Papers Warren A. Hunt Jr.
• [Hol-info] DeepLearn 2017: early registration January 27 GRLMC
• [Hol-info] Recent inconsistency in HOL/Isabelle a matter of an (unresolved) dependency; the LCF approach in HOL/Isabelle and other HOL systems (Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy) Ken Kubota
  • Re: [Hol-info] Recent inconsistency in HOL/Isabelle a matter of an (unresolved) dependency; the LCF approach in HOL/Isabelle and other HOL systems (Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy) Thomas Melham
• [Hol-info] CFP International Conference on Logic Programming and Non-monotonic Reasoning, Finland, 3-6 July 2017 Peter Schüller
  • [Hol-info] CFP International Conference on Logic Programming and Non-monotonic Reasoning, Finland, 3-6 July 2017 Peter Schüller
• [Hol-info] ACM/SPEC ICPE 2017 - Deadline Extension - Call for Posters and Demonstrations Andrea Rosa
• [Hol-info] CfP: Models for Formal Analysis of Real Systems (MARS 2017) Peter.Hoefner
• [Hol-info] Postdoc position in provably secure systems Roberto Guanciale
• [Hol-info] Final Call for Workshop Proposals: International Conference on Logic Programming and Nonmonotonic Reasoning, Espoo, Finland, July 3-6, 2017 Peter Schüller
• [Hol-info] LPAR-21 in Botswana - CFP Geoff Sutcliffe
• [Hol-info] QUse.use and exceptions Ramana Kumar
• [Hol-info] ACM/SPEC ICPE 2017 - Call for Posters and Demonstrations Andrea Rosa
• [Hol-info] CALCO 2017: First Call for Papers Fabio Zanasi
• [Hol-info] [fm-announcements] SPIN 2017 - 2nd Call for Papers *Paper Submission: February 10, 2017* Havelund, Klaus (348B)
• [Hol-info] ACSD 2017: Call-for-Papers Klaus Schneider
• [Hol-info] PhD positions on the AI4REASON project in Prague Josef Urban
• [Hol-info] SAFECOMP17 Call for Papers Stefano Tonetta
• [Hol-info] Call for Participation: Practical Aspects of Declarative Languages (PADL) Paris, France, January 16/17, 2017 Peter Schüller
• [Hol-info] 2017 ACL2 Workshop Call for Paper Warren A. Hunt Jr.
• [Hol-info] Similar trouble building HOL Light's pa_j.ml Geoffrey Irving
  • Re: [Hol-info] Similar trouble building HOL Light's pa_j.ml Rob Arthan
  • Re: [Hol-info] Similar trouble building HOL Light's pa_j.ml Geoffrey Irving
• [Hol-info] Call for Workshop Proposals: International Conference on Logic Programming and Nonmonotonic Reasoning, Espoo, Finland, July 3-6, 2017 Peter Schüller
• [Hol-info] PostDoc Positions on Planning and Scheduling in the Embedded System Research Unit Marco Roveri
• [Hol-info] 1st CFP: IMBSA 2017 - International Symposium on Model-Based Safety and Assessment Marco Bozzano
• [Hol-info] WiL 2017: Women in Logic Workshop Call for Papers Amy Felty
• [Hol-info] Henkin's paper "Completeness in the Theory of Types" (1950); Ramsey (and Chwistek) Ken Kubota
  • Re: [Hol-info] [Coq-Club] Henkin's paper "Completeness in the Theory of Types" (1950); Ramsey (and Chwistek) Hugo Herbelin
  • [Hol-info] Curry-Howard isomorphism - Re: [Coq-Club] Henkin's paper "Completeness in the Theory of Types" (1950); Ramsey (and Chwistek) Ken Kubota
  • [Hol-info] On the natural language of formal logic and mathematics - Re: [Coq-Club] Henkin's paper "Completeness in the Theory of Types" (1950); Ramsey (and Chwistek) Ken Kubota
• [Hol-info] Call for Participation - Hardware Design Contest Sponsored by ACM SIGDA Bei Yu
• [Hol-info] CfP RAMICS 2017 deadline extension Peter.Hoefner
• [Hol-info] LPAR-21 in Botswana - Call for Papeprs Geoff Sutcliffe
• [Hol-info] CAV 2017 Call for Workshop proposals Mikaël Mayer
• [Hol-info] Proving a trivial goal Scott Owens
  • Re: [Hol-info] Proving a trivial goal Johannes Åman Pohjola
  • Re: [Hol-info] Proving a trivial goal Ramana Kumar
• [Hol-info] ACM/SPEC ICPE 2017 - Call for Work in Progress and Vision Papers Andrea Rosa
• [Hol-info] 2nd CFP, NFM 2017: 9th NASA Formal Methods Symposium Guy Katz
• [Hol-info] TABLEAUX/FroCoS/ITP Call for Papers Geoff Sutcliffe
• [Hol-info] CADE-26 Call for Workshops, Tutorials, System Competition, and Papers Geoff Sutcliffe
• [Hol-info] [fm-announcements] SPIN 2017 - Call for papers Havelund, Klaus (348B)
• [Hol-info] CfP: MARS 2017 - Models for Formal Analysis of Real Systems Peter.Hoefner
• [Hol-info] Using HolyHammer Ramana Kumar
• [Hol-info] TPTP and Automated Reasoning Geoff Sutcliffe
• [Hol-info] ACM/SPEC ICPE 2017 - Call for Workshop Proposals Andrea Rosa
• [Hol-info] LATA 2017: extended submission deadline October 28 GRLMC
• [Hol-info] Artificial Intelligence and Theorem Proving - Call for Papers Geoff Sutcliffe
• [Hol-info] Who is ProofPower "by" (and STT)? Roger Bishop Jones
  • [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Ken Kubota
  • [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family Ken Kubota
  • Re: [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family Mark Adams
  • Re: [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family John . Harrison
  • [Hol-info] The HOL family, HOL Light, Q0, and type abstraction Ken Kubota
  • Re: [Hol-info] The HOL family, HOL Light, Q0, and type abstraction John . Harrison
  • [Hol-info] The definitional principles of HOL and equivalent mechanisms in Q0/R0 Ken Kubota
  • [Hol-info] Type quantifiers, definability of logical constants/quantifiers/connectives, equality, group theory (expressiveness with type abstraction) Ken Kubota
  • Re: [Hol-info] Type quantifiers, definability of logical constants/quantifiers/connectives, equality, group theory (expressiveness with type abstraction) Thomas Melham
  • [Hol-info] John's historical survey including Thomas Hales' proof, Dependent types in PVS Ken Kubota
  • Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Rob Arthan
  • Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Ondřej Kunčar
  • Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Scott Owens
  • Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Rob Arthan
  • [Hol-info] Consercative extension in HOL, some pre-history Roger Bishop Jones
  • Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Andrei Popescu
  • [Hol-info] Conditions under which model-theoretic conservativity entails proof-theoretic conservativity Roger Bishop Jones
  • Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Rob Arthan
  • Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Andrei Popescu
  • [Hol-info] conservativity of HOL constant and type definitions Andrei Popescu
  • Re: [Hol-info] conservativity of HOL constant and type definitions Rob Arthan
  • Re: [Hol-info] conservativity of HOL constant and type definitions Ondřej Kunčar
  • Re: [Hol-info] conservativity of HOL constant and type definitions Rob Arthan
  • Re: [Hol-info] conservativity of HOL constant and type definitions Ondřej Kunčar
  • Re: [Hol-info] conservativity of HOL constant and type definitions Andrei Popescu
  • Re: [Hol-info] conservativity of HOL constant and type definitions Ramana Kumar
  • Re: [Hol-info] conservativity of HOL constant and type definitions Andrei Popescu
  • Re: [Hol-info] conservativity of HOL constant and type definitions Ondřej Kunčar
• [Hol-info] ITP 2017 - FIRST CALL FOR PAPERS Cláudia Nalon
• [Hol-info] DL 2017, Call for Papers Geoff Sutcliffe
  • [Hol-info] DL 2017, Call for Papers Geoff Sutcliffe
• [Hol-info] CFP International Conference on Logic Programming and Non-monotonic Reasoning, Finland, July 3-5, 2017 Peter Schüller
• [Hol-info] NFM 2017 - Call For Workshops Rody Kersten
• [Hol-info] TPNC 2016: call for posters GRLMC
• [Hol-info] BigDat 2017: early registration October 21 GRLMC
• [Hol-info] AI Communications: Special Issue on Automated Reasoning Geoff Sutcliffe
• [Hol-info] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940) Ken Kubota
  • Re: [Hol-info] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940) Rob Arthan
  • Re: [Hol-info] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940) Ken Kubota
• [Hol-info] ACM/SPEC ICPE 2017 - Call for Tutorial Proposals Andrea Rosa
• [Hol-info] Evaluation in HOL-Light Heiko Becker
  • Re: [Hol-info] Evaluation in HOL-Light John . Harrison
• [Hol-info] change of email address Brian Graham
  • Re: [Hol-info] change of email address Ramana Kumar
• [Hol-info] LATA 2017: 3rd call for papers GRLMC
• [Hol-info] Helmut Veith Stipend Georg Weissenbacher
• [Hol-info] Open Ph.D. position in Formal Methods for Information Security at ETH Zurich Ralf Sasse
• [Hol-info] ACM/SPEC ICPE 2017 - Deadline Extension Andrea Rosa
• [Hol-info] CFP, deadline Oct. 5: The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP'17) Yves Bertot
• [Hol-info] Error Loading Theory in HOL Light Adnan Rashid
  • Re: [Hol-info] Error Loading Theory in HOL Light John . Harrison
  • Re: [Hol-info] Error Loading Theory in HOL Light Cris Perdue
  • Re: [Hol-info] Error Loading Theory in HOL Light Adnan Rashid
  • Re: [Hol-info] Error Loading Theory in HOL Light John . Harrison
  • Re: [Hol-info] Error Loading Theory in HOL Light Petros Papapanagiotou
• [Hol-info] TABLEAUX, FroCoS, ITP - Call for Workshops and Tutorials Joao Marcos
  • [Hol-info] TABLEAUX, FroCoS, ITP - Call for Workshops and Tutorials Geoff Sutcliffe
• [Hol-info] Questions about Embedding VHDL Dwi Teguh Priyantini
• [Hol-info] ACM/SPEC ICPE 2017 - 3rd Call for Papers Andrea Rosa
• [Hol-info] LATA 2017: 2nd call for papers GRLMC
• [Hol-info] GCAI 2016 - Call for Participation Geoff Sutcliffe
• Re: [Hol-info] [Coq-Club] is the axiom of choice... ? Ken Kubota
  • [Hol-info] Proof without the Axiom of Choice (was: Fwd: [Coq-Club] is the axiom of choice... ?) Ken Kubota
• [Hol-info] [CFP] RAMiCS 2017 Damien Pous
  • [Hol-info] [CFP] RAMiCS 2017 Damien Pous
• [Hol-info] ICLP 2016 Call for Participation - Early Registration deadline Mon Sep 5, 2016 Peter Schüller
• [Hol-info] SETTA 2016 - Call for Participation - Symposium on Dependable Software Engineering Theories, Tools and Applications Beijing, China, Nov. 9-11, 2016 Nils Muellner
• [Hol-info] Practical considerations (automation) vs. "pure" logic (expressiveness/reducibility) Ken Kubota
• [Hol-info] CFP NFM 2017: 9th NASA Formal Methods Symposium Guy Katz
• [Hol-info] ACM/SPEC ICPE 2017 - 2nd Call for Papers Andrea Rosa
• [Hol-info] Call for Participation: ICLP, New York City, Oct 16-21, 2016: International Conference on Logic Programming Peter Schueller
• [Hol-info] Last Call for Participation: LOPSTR 2016 - 26th Intl. Symp. on Logic-Based Program Synthesis and Transformation Pedro López García
• [Hol-info] CALL FOR PAPERS: Special Issue on Milestones in Interactive Theorem Proving Lawrence Paulson
• [Hol-info] Theory documentation outside of HOL Corey Richardson
  • Re: [Hol-info] Theory documentation outside of HOL Michael.Norrish
• [Hol-info] HOL4 on Mac OS X using the ML variant shipped with Isabelle Ken Kubota
  • Re: [Hol-info] HOL4 on Mac OS X using the ML variant shipped with Isabelle Michael.Norrish
• [Hol-info] Literature on the type system of Isabelle/HOL; text by Mike Gordon Ken Kubota
  • Re: [Hol-info] [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon Lawrence Paulson
  • [Hol-info] Literature on the type system of Isabelle/HOL; HOL documentation; non-logical axioms vs. definitions; epsilon vs. description operator (HOL vs. Q0); Rule R of Andrews' logic Q0 Ken Kubota
  • [Hol-info] HOL documentation; epsilon vs. description operator (HOL vs. Q0) Ken Kubota
  • Re: [Hol-info] HOL documentation; epsilon vs. description operator (HOL vs. Q0) Thomas Melham
• [Hol-info] Emacs indentation for theory scripts Corey Richardson
  • Re: [Hol-info] Emacs indentation for theory scripts Michael.Norrish
• [Hol-info] ICLA 2017 Call for Papers Geoff Sutcliffe
• [Hol-info] Call for Participation: ICLP, New York City: International Conference on Logic Programming, Oct 17-21, 2016 Peter Schueller
• [Hol-info] Postdoctoral position, concurrency reasoning, Imperial College London Gardner, Philippa A
• [Hol-info] Using pattern_matches's custom syntax Armaël Guéneau
  • Re: [Hol-info] Using pattern_matches's custom syntax Thomas Tuerk
  • Re: [Hol-info] Using pattern_matches's custom syntax Michael.Norrish
• [Hol-info] Managed Languages & Runtimes Week '16 - Call for Participation Andrea Rosa
• [Hol-info] FORMATS 2016 - Call for participation Sebastian Gerwinn
• [Hol-info] EVAL(tac conv rule) hamed nemati
  • Re: [Hol-info] EVAL(tac conv rule) Michael.Norrish
  • Re: [Hol-info] EVAL(tac conv rule) hamed nemati
  • Re: [Hol-info] EVAL(tac conv rule) Michael.Norrish
• [Hol-info] Questions about basic logic gates in HOL/HOL Light dwi.teguh51
  • Re: [Hol-info] Questions about basic logic gates in HOL/HOL Light Thomas Melham
• [Hol-info] Call For Participation: WADT 2016 JAMES P. (366409)
• Re: [Hol-info] hol-info Digest, Vol 122, Issue 1 Abid Rauf
• [Hol-info] Corrections of and amendments to prior publications on Goedel's First Incompleteness Theorem; Russell O'Connor's definitions for its proof in Peter B. Andrews' logic Q0; Comparison of the proofs by O'Connor and Paulson Ken Kubota
• [Hol-info] VTSA summer school Stephan Merz
• [Hol-info] Rewriting and Types in HOL-Light Heiko Becker
  • Re: [Hol-info] Rewriting and Types in HOL-Light Petros Papapanagiotou
  • Re: [Hol-info] Rewriting and Types in HOL-Light Heiko Becker
  • Re: [Hol-info] Rewriting and Types in HOL-Light Marco Maggesi
• [Hol-info] Deriving Contradictions Heiko Becker

• Earlier messages
• Later messages