[Hol-info] Type abstraction – Re: Mike Gordon bio

Not quite a correction, but an important addendum to the last part ("Legacy") is type abstraction, which Mike Gordon suggested for HOL (but didn't implement), shaping future research. He already foresaw a binding of variables connecting both term and type (subscript) level. (Gordon positively

Re: [Hol-info] Extension of Co-algebraic Datatype

Hi Waqar, I think you’re looking for a datatype package in which induction and coinduction types can be mixed naturally. This is currently not possible in HOL4, but it’s not the fault of Higher Order Logic itself. According to Andrei Popescu et al. [1] it’s in theory possible to port or

[Hol-info] 1st Call for Papers Software Verification and Testing Track @ ACM SAC 2019

34th Annual ACM Symposium on Applied Computing Software Verification and Testing Track Limassol, Cyprus April 8 – 12, 2019 https://www.sigapp.org/sac/sac2019/

[Hol-info] Second Call for Papers: FSEN 2019

## SECOND CALL FOR PAPERS Eighth International Conference on Fundamentals of Software Engineering 2019 - Theory and Practice (FSEN '19) http://fsen.ir/2019 Tehran, Iran May 1-3, 2019

[Hol-info] PPDP 2018: Call for Participation

==     PPDP 2018: Call for Participation == 20th International Symposium on     Principles and Practice of Declarative

Re: [Hol-info] Extension of Co-algebraic Datatype

Hi, In Isabelle, besides coinduction, the normal induction procedure on lazylist/stream datatype appears to be allowed.. Can a same behaviour is possible with the 'a llist type in HOL4. Secondly, unlike lazy list, the "stream" are defined without having the empty "LNIL". I see a similar

Re: [Hol-info] VTSA 2018: call for applications

Although the deadline for application has passed, a few places remain available. If you are interested, please send the indicated documents to stephan.m...@loria.fr : registrations remain possible until the remaining slots have been filled. Thank you, Stephan Merz