hol-info

Messages by Date

2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Chun Tian (binghe)
2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Ramana Kumar
2017/10/05 [Hol-info] Definitions of partial functions (incl. predicates) Mario Castelán Castro
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Freek Wiedijk
2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Chun Tian (binghe)
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Mario Castelán Castro
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Jeremy Dawson
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Mario Castelán Castro
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Chun Tian (binghe)
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Jeremy Dawson
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Jeremy Dawson
2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Chun Tian (binghe)
2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Scott Owens
2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Chun Tian (binghe)
2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Chun Tian (binghe)
2017/10/05 Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Konrad Slind
2017/10/05 [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list? Chun Tian (binghe)
2017/10/05 [Hol-info] LRTC (Reflexive Transitive Closure with a List) Chun Tian (binghe)
2017/10/05 Re: [Hol-info] Changing thms used by computeLib Ramana Kumar
2017/10/05 Re: [Hol-info] Changing thms used by computeLib Heiko Becker
2017/10/05 Re: [Hol-info] Changing thms used by computeLib Ramana Kumar
2017/10/05 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Freek Wiedijk
2017/10/05 [Hol-info] Changing thms used by computeLib Heiko Becker
2017/10/04 Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems Ramana Kumar
2017/09/29 Re: [Hol-info] Is it possible to make Holmake print timing information? Mario Castelán Castro
2017/09/29 Re: [Hol-info] Is it possible to make Holmake print timing information? Mario Castelán Castro
2017/09/29 Re: [Hol-info] Is it possible to make Holmake print timing information? Ramana Kumar
2017/09/28 Re: [Hol-info] Question on rewriting with assumptions Mario Castelán Castro
2017/09/28 Re: [Hol-info] Is it possible to make Holmake print timing information? Mario Castelán Castro
2017/09/27 [Hol-info] Commonsense-2017 - Call for Participation geoff
2017/09/27 Re: [Hol-info] Is it possible to make Holmake print timing information? Chun Tian (binghe)
2017/09/27 [Hol-info] Is it possible to make Holmake print timing information? Mario Castelán Castro
2017/09/26 Re: [Hol-info] Is it possible to make Holmake print timing information? Ramana Kumar
2017/09/26 Re: [Hol-info] Question on rewriting with assumptions Ramana Kumar
2017/09/26 Re: [Hol-info] Is it possible to make Holmake print timing information? Michael.Norrish
2017/09/25 Re: [Hol-info] Question on rewriting with assumptions Mario Castelán Castro
2017/09/25 Re: [Hol-info] Question on rewriting with assumptions Mario Castelán Castro
2017/09/25 Re: [Hol-info] Question on rewriting with assumptions Chun Tian (binghe)
2017/09/25 [Hol-info] Question on rewriting with assumptions Mario Castelán Castro
2017/09/25 Re: [Hol-info] Question on rewriting with assumptions Thomas Tuerk
2017/09/22 [Hol-info] LATA 2018: 1st call for papers GRLMC
2017/09/19 [Hol-info] [Vardi-list] Advanced Winter School on Formal Verification Moshe Vardi
2017/09/18 [Hol-info] KR 2018 Doctoral Consortium Call for Papers Marcello Balduccini
2017/09/18 [Hol-info] KR18 - Preliminary Call for Tutorial and Workshop Proposals Marcello Balduccini
2017/09/18 [Hol-info] KR 2018 Call for Papers Marcello Balduccini
2017/09/16 [Hol-info] FINAL call for papers: CPP 2018 Amy Felty
2017/09/14 [Hol-info] Experience and opinions on proof assistants with “rich” type systems Mario Castelán Castro
2017/09/14 Re: [Hol-info] A small question about Datatype. Michael.Norrish
2017/09/14 [Hol-info] A small question about Datatype. Liu Gengyang
2017/09/14 [Hol-info] [fm-announcements] NASA Formal Methods Symposium 2018 - CFP Munoz, Cesar (LARC-D320)
2017/09/13 [Hol-info] ABZ 2018, Call for Contributions Asieh Salehi
2017/09/12 [Hol-info] Now online: ML for the Working Programmer Lawrence Paulson
2017/09/11 Re: [Hol-info] How to find existing developments in HOL4? Mario Castelán Castro
2017/09/11 Re: [Hol-info] How to find existing developments in HOL4? Mario Castelán Castro
2017/09/11 Re: [Hol-info] How to find existing developments in HOL4? Ramana Kumar
2017/09/11 Re: [Hol-info] How to find existing developments in HOL4? Chun Tian (binghe)
2017/09/11 [Hol-info] SOAP@SAC 2018, April 9-13, Pau, France - (EXTENDED DEADLINE) final call for papers sac . soap2018
2017/09/10 Re: [Hol-info] How to find existing developments in HOL4? John . Harrison
2017/09/10 [Hol-info] [Reminder] PADL 2018 - abstract deadline approaching manna
2017/09/10 [Hol-info] CfPart: Reliability, safety and security of railway systems - RSSRail 2017 (Pistoia, Italy) Alexander Romanovsky
2017/09/10 Re: [Hol-info] How to find existing developments in HOL4? Mario Castelán Castro
2017/09/10 [Hol-info] How to find existing developments in HOL4? Mario Castelán Castro
2017/09/08 Re: [Hol-info] [SOLVED] Theorems used by an invocation of simp, fs, rw or REWRITE_TAC. Mario Castelán Castro
2017/09/08 [Hol-info] Theorems used by an invocation of simp, fs, rw or REWRITE_TAC. Mario Castelán Castro
2017/09/08 Re: [Hol-info] Instantiating type variables Heiko Becker
2017/09/08 Re: [Hol-info] Instantiating type variables Anthony Fox
2017/09/08 [Hol-info] Instantiating type variables Heiko Becker
2017/09/06 Re: [Hol-info] About restricted quantification and algebraic-like structures Mario Castelán Castro
2017/09/06 [Hol-info] IJCAR 2018 - Calll for Papers geoff
2017/09/06 Re: [Hol-info] About restricted quantification and algebraic-like structures Michael.Norrish
2017/09/05 Re: [Hol-info] About restricted quantification and algebraic-like structures Mario Castelán Castro
2017/09/05 Re: [Hol-info] About restricted quantification and algebraic-like structures Michael.Norrish
2017/09/04 [Hol-info] About restricted quantification and algebraic-like structures Mario Castelán Castro
2017/09/04 [Hol-info] [Last CfP] PADL 2018 - abstract deadline EXTENDED TO SEPTEMBER 10, 2017 manna
2017/09/02 Re: [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light? Mario Castelán Castro
2017/09/02 Re: [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light? Chun Tian (binghe)
2017/09/02 Re: [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light? Mario Castelán Castro
2017/09/02 [Hol-info] CFP: 2018 IEEE/ACM Design Automation Conference Hardware Design Contest Yiyu Shi
2017/09/01 Re: [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light? Mario Carneiro
2017/09/01 [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light? Ken Kubota
2017/09/01 [Hol-info] [CfP] PADL 2018 - abstract submission DEADLINE APPROACHING manna
2017/08/31 [Hol-info] CfP ThEdu'17 post-proceedings Walther Neuper
2017/08/30 [Hol-info] FMCAD 2017 (Call for participation: early registration ends Sept 2) Georg Weissenbacher
2017/08/30 [Hol-info] FACS 2017 - Doctoral Track: Call for Contributions Jose Proenca
2017/08/30 [Hol-info] What is the practical (end-user level) difference between HOL4 and HOL Light? Mario Castelán Castro
2017/08/30 Re: [Hol-info] Handling existentials in conclusions Heiko Becker
2017/08/30 [Hol-info] Handling existentials in conclusions Heiko Becker
2017/08/29 [Hol-info] International Workshop on Testing Extra-Functional Properties and Quality Characteristics of Software Systems (ITEQS) Nils Muellner
2017/08/29 [Hol-info] FMCAD 2017: CALL FOR PARTICIPATION geoff
2017/08/29 [Hol-info] PPDP and LOPSTR 2017 Call for Participation Wim Vanhoof
2017/08/23 Re: [Hol-info] Strange tactics bug when using match_mp_tac Michael.Norrish
2017/08/23 Re: [Hol-info] Strange tactics bug when using match_mp_tac Ramana Kumar
2017/08/23 Re: [Hol-info] Strange tactics bug when using match_mp_tac Michael.Norrish
2017/08/23 [Hol-info] ACM/SPEC ICPE 2018: Call for Contributions ICPE ICPE
2017/08/23 [Hol-info] SAFECOMP17 Last Call for Participation Stefano Tonetta
2017/08/23 Re: [Hol-info] Strange tactics bug when using match_mp_tac Heiko Becker
2017/08/23 Re: [Hol-info] Strange tactics bug when using match_mp_tac Jeremy Dawson
2017/08/23 [Hol-info] MEMOCODE-2017 (Call for Participation) Klaus . Schneider
2017/08/23 Re: [Hol-info] Strange tactics bug when using match_mp_tac Michael.Norrish
2017/08/22 [Hol-info] Strange tactics bug when using match_mp_tac Heiko Becker
2017/08/22 Re: [Hol-info] Sad news regarding Mike Gordon Mario Castelán Castro
2017/08/22 [Hol-info] Fwd: [mike-gordon-update] sad news Konrad Slind
2017/08/22 Re: [Hol-info] Sad news regarding Mike Gordon Chun Tian (binghe)
2017/08/22 [Hol-info] Sad news regarding Mike Gordon Kalvala, Sara
2017/08/22 [Hol-info] GCAI in Miami - Call for Posters geoff
2017/08/21 Re: [Hol-info] Indentation of proof script in Emacs Mario Castelán Castro
2017/08/20 Re: [Hol-info] Indentation of proof script in Emacs Michael.Norrish
2017/08/20 Re: [Hol-info] Indentation of proof script in Emacs Mario Castelán Castro
2017/08/20 Re: [Hol-info] Indentation of proof script in Emacs Chun Tian (binghe)
2017/08/20 [Hol-info] 3rd CfP: PADL 2018 - 20th International Symposium on Practical Aspects of Declarative Languages manna
2017/08/19 [Hol-info] Indentation of proof script in Emacs Mario Castelán Castro
2017/08/15 [Hol-info] FMCAD 2017: CALL FOR PARTICIPATION no-reply
2017/08/13 [Hol-info] KR18 - Preliminary Call for Tutorial and Workshop Proposals Marcello Balduccini
2017/08/13 [Hol-info] CfP: Relational and Algebraic Methods in Computer Science - Special Issue in JLAMP Peter.Hoefner
2017/08/11 [Hol-info] SOAP@SAC 2017, April 9-13, Pau, France - second call for papers sac . soap2018
2017/08/09 [Hol-info] TPTP v7.0.0 and CASC-26 geoff
2017/08/09 [Hol-info] [fm-announcements] RV 2017 - 2nd Call for Participation Havelund, Klaus (348B)
2017/08/07 Re: [Hol-info] How to reduce these lambda equations to F? Chun Tian (binghe)
2017/08/06 Re: [Hol-info] How to reduce these lambda equations to F? Michael.Norrish
2017/08/06 [Hol-info] PADL 2018 - 1 month to abstract deadline manna
2017/08/06 [Hol-info] FOCLASA 2017 - Call for Participation foclasa2017
2017/08/04 Re: [Hol-info] How to reduce these lambda equations to F? Chun Tian (binghe)
2017/08/04 [Hol-info] CPP 2018 2nd call for papers Amy Felty
2017/08/04 Re: [Hol-info] How to reduce these lambda equations to F? Thomas Tuerk
2017/08/04 [Hol-info] How to reduce these lambda equations to F? Chun Tian (binghe)
2017/08/01 [Hol-info] SLSP 2017: call for posters GRLMC
2017/07/29 [Hol-info] TABLEAUX 2017, FroCoS 2017, ITP 2017 - Call for Participation geoff
2017/07/24 Re: [Hol-info] On the use of new_axiom() in formal projects Andrei Popescu
2017/07/24 [Hol-info] Coquand on HOL; similarity to Q – Re: On the use of new_axiom() in formal projects Ken Kubota
2017/07/24 Re: [Hol-info] On the use of new_axiom() in formal projects Andrei Popescu
2017/07/24 Re: [Hol-info] On the use of new_axiom() in formal projects Andrei Popescu
2017/07/24 Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects Ramana Kumar
2017/07/24 Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects Chun Tian (binghe)
2017/07/23 Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects Michael.Norrish
2017/07/23 Re: [Hol-info] How to write a general EQ_CONV ? Chun Tian (binghe)
2017/07/22 Re: [Hol-info] How to write a general EQ_CONV ? Konrad Slind
2017/07/22 [Hol-info] How to write a general EQ_CONV ? Chun Tian (binghe)
2017/07/22 Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects Chun Tian (binghe)
2017/07/21 Re: [Hol-info] On the use of new_axiom() in formal projects Andrei Popescu
2017/07/21 Re: [Hol-info] On the use of new_axiom() in formal projects Chun Tian (binghe)
2017/07/20 [Hol-info] [fm-announcements] RV 2017 - 1st Call for Participation Havelund, Klaus (348B)
2017/07/20 [Hol-info] SEFM 2017 -- Call for Participation Alberto Griggio
2017/07/19 [Hol-info] Open PostDoc Positions Martin Leucker
2017/07/19 [Hol-info] Open PhD positions Martin Leucker
2017/07/17 [Hol-info] DATE 2018 Formal Methods and Verification Track (D4) Schmaltz, J.
2017/07/17 [Hol-info] KR 2018 Preliminary Call for Papers Marcello Balduccini
2017/07/13 Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects Chun Tian (binghe)
2017/07/13 Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() in formal projects Michael.Norrish
2017/07/13 Re: [Hol-info] On the use of new_axiom() in formal projects Michael.Norrish
2017/07/13 Re: [Hol-info] On the use of new_axiom() in formal projects Chun Tian (binghe)
2017/07/13 Re: [Hol-info] On the use of new_axiom() in formal projects Ramana Kumar
2017/07/13 [Hol-info] On the use of new_axiom() in formal projects Chun Tian (binghe)
2017/07/13 Re: [Hol-info] A question about ordinals Chun Tian (binghe)
2017/07/12 Re: [Hol-info] Vimhol key binding for showtypes Ramana Kumar
2017/07/12 Re: [Hol-info] A question about ordinals Michael.Norrish
2017/07/12 Re: [Hol-info] A question about ordinals Chun Tian (binghe)
2017/07/12 Re: [Hol-info] A question about ordinals Ramana Kumar
2017/07/12 Re: [Hol-info] A question about ordinals Chun Tian (binghe)
2017/07/12 Re: [Hol-info] A question about ordinals Chun Tian (binghe)
2017/07/12 Re: [Hol-info] A question about ordinals Chun Tian (binghe)
2017/07/12 [Hol-info] A question about ordinals Chun Tian (binghe)
2017/07/11 [Hol-info] Proof kernel, Pollack-consistency and faithfulness – Re: [isabelle] Verify the legitimacy of a proof? Ken Kubota
2017/07/11 Re: [Hol-info] Counting Subgoals in a Proof Konrad Slind
2017/07/11 Re: [Hol-info] Counting Subgoals in a Proof Thomas Tuerk
2017/07/11 [Hol-info] Counting Subgoals in a Proof Matthias Stockmayer
2017/07/10 [Hol-info] SOAP@SAC 2017, April 9-13, Pau, France - call for papers sac . soap2018
2017/07/10 Re: [Hol-info] Vimhol key binding for showtypes Robert Künnemann
2017/07/10 Re: [Hol-info] How to define "infinite sums" of custom datatypes? Chun Tian (binghe)
2017/07/10 [Hol-info] CfP: PADL 2018 - 20th International Symposium on Practical Aspects of Declarative Languages manna
2017/07/09 Re: [Hol-info] How to define "infinite sums" of custom datatypes? Michael.Norrish
2017/07/09 [Hol-info] Vimhol key binding for showtypes Ramana Kumar
2017/07/09 [Hol-info] Concept of a small logical kernel, preserving logical dependencies, axiomatic type classes vs. type abstraction, Isabelle documentation – Re: [isabelle] Verify the legitimacy of a proof? Ken Kubota
2017/07/05 Re: [Hol-info] How to define "infinite sums" of custom datatypes? Chun Tian (binghe)
2017/07/05 Re: [Hol-info] Choosing an element from an infinite set according to an equivalence relation and a finite set? Chun Tian (binghe)
2017/07/04 [Hol-info] Funded PhD positions at Edinburgh verifying embedded ARM security Ian Stark
2017/07/04 [Hol-info] FIRST Call For Papers: FLOPS 2018: 14th International Symposium on Functional and Logic Programming John Patrick Gallagher
2017/07/03 [Hol-info] Choosing an element from an infinite set according to an equivalence relation and a finite set? Chun Tian (binghe)
2017/07/03 [Hol-info] How to define "infinite sums" of custom datatypes? Chun Tian (binghe)
2017/07/03 [Hol-info] [fm-announcements] RV-CuBES Deadline Extension Havelund, Klaus (348B)
2017/07/02 Re: [Hol-info] What's the recommended way to delete elements from list? Chun Tian (binghe)
2017/07/02 Re: [Hol-info] What's the recommended way to delete elements from list? Ramana Kumar
2017/07/02 [Hol-info] What's the recommended way to delete elements from list? Chun Tian (binghe)
2017/07/01 Re: [Hol-info] Difficulties in proving the termination of a recursive function Ramana Kumar
2017/07/01 Re: [Hol-info] Difficulties in proving the termination of a recursive function Chun Tian (binghe)
2017/07/01 Re: [Hol-info] Difficulties in proving the termination of a recursive function Chun Tian (binghe)
2017/07/01 Re: [Hol-info] Difficulties in proving the termination of a recursive function Chun Tian (binghe)
2017/07/01 Re: [Hol-info] Difficulties in proving the termination of a recursive function Chun Tian (binghe)
2017/07/01 Re: [Hol-info] Difficulties in proving the termination of a recursive function Ramana Kumar
2017/07/01 Re: [Hol-info] Difficulties in proving the termination of a recursive function Konrad Slind
2017/07/01 [Hol-info] Difficulties in proving the termination of a recursive function Chun Tian (binghe)
2017/06/28 [Hol-info] PhD position in IoT Gwen Salaün
2017/06/26 [Hol-info] Encyclopedia of Proof Systems: Second Call for Encyclopedia Entries Bruno Woltzenlogel Paleo
2017/06/26 Re: [Hol-info] Different variable orders between GENL and Q.GENL Michael.Norrish
2017/06/26 [Hol-info] Different variable orders between GENL and Q.GENL Chun Tian (binghe)
2017/06/25 [Hol-info] Pollack-consistency and Faithfulness – Re: [Metamath] Articles on Hale[s'] Kepler Conjecture proof Ken Kubota
2017/06/25 Re: [Hol-info] [Metamath] Articles on Hale's Kepler Conjecture proof Mark Adams
2017/06/20 [Hol-info] Final Call for Papers: CICLOPS 2017 - 15th International Colloquium on Implementation of Constraint and LOgic Programming Systems (DEADLINES EXTENSION) Nataliia Stulova
2017/06/20 [Hol-info] GCAI 2017 in Miami - Call for Papers Geoff Sutcliffe
2017/06/20 Re: [Hol-info] [Metamath] Articles on Hale's Kepler Conjecture proof Ken Kubota
2017/06/20 [Hol-info] ITP / FLOC 2018 workshop application deadline Jeremy Avigad