hol-info  

Messages by Thread

• [Hol-info] MEMOCODE-2017 (Call for Papers) Klaus . Schneider
  • [Hol-info] MEMOCODE-2017 (Call for Papers) Klaus . Schneider
• [Hol-info] [fm-announcements] ITP 2017 - Final Call for Papers Munoz, Cesar (LARC-D320)
• [Hol-info] LPAR-21 Short Presentation Papers - Call for Papers Geoff Sutcliffe
• [Hol-info] TABLEAUX 2017 - Final Call for Papers Cláudia Nalon
• [Hol-info] [fm-announcements] RERS: International Challenge on the Rigorous Examination of Reactive Systems 2017 Havelund, Klaus (348B)
• [Hol-info] 3rd CFP: SEFM 2017 - 15th International Conference on Software Engineering and Formal Methods Alberto Griggio
• [Hol-info] Release of HOL4 Kananaskis-11 Michael.Norrish
• [Hol-info] First CFP Synasc 2017, Timisoara, Romania Isabela Dramnesc
• [Hol-info] [ICLP 2017] Second Call for Papers Tommaso.Urli
• [Hol-info] Marktoberdorf Summer School: Call for Participation Tobias Nipkow
• [Hol-info] [fm-announcements] RV 2017 - 2nd Call for papers and tutorials Havelund, Klaus (348B)
• [Hol-info] CfP Software Engineering for Resilient Systems - SERENE 2017 workshop Alexander Romanovsky
• [Hol-info] MFCS 2017: First Call for Papers Giorgio Bacci
• [Hol-info] SAFECOMP17 Extended Deadline Stefano Tonetta
• [Hol-info] CfP: FACS 2017 - 14th International Conference on Formal Aspects of Component Software Jose Proenca
• [Hol-info] Deadline Extension: IMBSA 2017 - International Symposium on Model-Based Safety and Assessment Marco Bozzano
• [Hol-info] NFM 2017 - Call For Participation Rody Kersten
  • [Hol-info] NFM 2017 - 2nd Call For Participation Rody Kersten
• [Hol-info] AlCoB 2017: call for posters GRLMC
  • [Hol-info] AlCoB 2017: call for posters GRLMC
• [Hol-info] DICE-FOPARA 2017: Deadline Extended Georg Moser
• [Hol-info] CFP ThEdu'17 at CADE 26 Walther Neuper
• [Hol-info] VSTTE 2017 - First Call for Papers Andrei Paskevich
• [Hol-info] Final CFP: IMBSA 2017 - International Symposium on Model-Based Safety and Assessment Marco Bozzano
• [Hol-info] Pollack-consistency (HOL Light, Isabelle, and others); Introductions to HOL4 and HOL Zero Ken Kubota
  • Re: [Hol-info] Pollack-consistency (HOL Light, Isabelle, and others); Introductions to HOL4 and HOL Zero Mark Adams
  • Re: [Hol-info] Pollack-consistency (HOL Light, Isabelle, and others); Introductions to HOL4 and HOL Zero Ken Kubota
  • [Hol-info] Correction on Hilbert-style systems (Metamath) and comment on prooftoys.org / mathtoys.org Ken Kubota
• [Hol-info] CfP: Reliability, safety and security of railway systems (RSSRail 2017) Alexander Romanovsky
  • [Hol-info] CfP: Reliability, safety and security of railway systems (RSSRail 2017) Alexander Romanovsky
  • [Hol-info] CfP: Reliability, safety and security of railway systems (RSSRail 2017) Alexander Romanovsky
• [Hol-info] DICE-FOPARA 2017 - Second Call for Papers Georg Moser
• [Hol-info] [fm-announcements] SPIN 2017 - Paper Submission: Extended to February 17 Havelund, Klaus (348B)
• [Hol-info] ARCADE Call for Papers Dmitriy Traytel
  • [Hol-info] ARCADE Call for Papers Geoff Sutcliffe
• [Hol-info] FORTE 2017: Deadline Extension Alexandra Silva
• [Hol-info] [CFP] CrossFyre 2017 Cristina Onete
• [Hol-info] SAFECOMP17 2nd Call for Papers Stefano Tonetta
• [Hol-info] Research officer in theoretical foundations of cyber security at Swansea University Markus Roggenbach
• [Hol-info] LATA 2017: call for participation GRLMC
• [Hol-info] How to correctly define a binder (as pretty printer)? Chun Tian (binghe)
  • Re: [Hol-info] How to correctly define a binder (as pretty printer)? Michael.Norrish
  • Re: [Hol-info] How to correctly define a binder (as pretty printer)? Chun Tian (binghe)
• [Hol-info] WiL 2017: Women in Logic Workshop Second Call for Papers (new dates) Amy Felty
• [Hol-info] CALCO 2017: Second Call for Papers Fabio Zanasi
• [Hol-info] TbILLC 2017: 1st Call for Papers Alexandra Silva
• [Hol-info] Open PhD position in Pesto team at Inria Nancy - Grand Est Steve Kremer
• [Hol-info] IWIL 2017 with LPAR-21 in Botswana - Call for Papers Geoff Sutcliffe
• [Hol-info] CfPart: FSEN 2017 Marjan Sirjani
• [Hol-info] Final CFP with Deadline Extension: LPNMR - International Conference on Logic Programming and Non-monotonic Reasoning, Finland, 3-6 July 2017 Peter Schüller
• [Hol-info] Automated Formal Methods (AFM) 2017 Call for papers Sam Owre
• [Hol-info] FroCoS 2017 - 2nd Call for Papers Geoff Sutcliffe
• [Hol-info] CfP FMCAD 2017 - Formal Methods in Computer Aided Design no-reply
  • [Hol-info] CfP FMCAD 2017 - Formal Methods in Computer Aided Design no-reply
• [Hol-info] ITP 2017 - 2nd Call for Papers Geoff Sutcliffe
• [Hol-info] ITP 2017 - Second Call for Papers Cláudia Nalon
• [Hol-info] [fm-announcements] SPIN 2017 - final call for papers, deadline Feb 10 Havelund, Klaus (348B)
• [Hol-info] FroCoS 2017 - Second Call for Papers Cláudia Nalon
• [Hol-info] deactivate newline-and-indent for sml-mode Heiko Becker
  • Re: [Hol-info] deactivate newline-and-indent for sml-mode Thomas Tuerk
  • Re: [Hol-info] deactivate newline-and-indent for sml-mode Heiko Becker
  • Re: [Hol-info] deactivate newline-and-indent for sml-mode Chun Tian (binghe)
  • Re: [Hol-info] deactivate newline-and-indent for sml-mode Thomas Tuerk
  • Re: [Hol-info] deactivate newline-and-indent for sml-mode Magnus Myreen
  • Re: [Hol-info] deactivate newline-and-indent for sml-mode Heiko Becker
• [Hol-info] First Call for Papers - 10th Conference on Intelligent Computer Mathematics - CICM 2017 - Abstract Submission Deadline 15. March 2017 Serge Autexier
• [Hol-info] How to convert an EQ theorem to IMP theorem? Chun Tian (binghe)
  • Re: [Hol-info] How to convert an EQ theorem to IMP theorem? Chun Tian (binghe)
• [Hol-info] ICLP 2017 - Call for Workshop Proposals Enrico Pontelli
• [Hol-info] 2nd CFP: IMBSA 2017 - International Symposium on Model-Based Safety and Assessment Marco Bozzano
• [Hol-info] CAV 2017 Award mikael . mayer
• [Hol-info] CAV 2017: Call for Papers mikael . mayer
• [Hol-info] JAR Special Issue on Automated Reasoning Systems Geoff Sutcliffe
  • [Hol-info] JAR Special Issue on Automated Reasoning Systems Geoff Sutcliffe
• [Hol-info] FMCAD 2017 - Call for Papers Geoff Sutcliffe
• [Hol-info] How to transform an assumption without touching the goal? Chun Tian (binghe)
  • Re: [Hol-info] How to transform an assumption without touching the goal? Ramana Kumar
  • Re: [Hol-info] How to transform an assumption without touching the goal? Chun Tian (binghe)
• [Hol-info] CfP: FMCAD 2017 - Formal Methods in Computer Aided Design Georg Weissenbacher
• [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Thomas Tuerk
  • Re: [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Thomas Tuerk
  • Re: [Hol-info] How to prove this theorem about relations? Chun Tian (binghe)
  • Re: [Hol-info] How to prove this theorem about relations? Thomas Tuerk
  • 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

• Earlier messages
• Later messages