ABSTRACT. Recently, HOL4 has been successfully used in both the formalization of pure mathematics (e.g., extended real number theory and fractional calculus) and verification of engineering systems (e.g., wireless sensor networks, communication protocols). The aim of this talk is twofold: First, presenting the perspective of non-computer science community such as physicist or an engineer. We will also present some suggestions which can be helpful in extending the user community of HOL4 in new fields such as physics, biology, and economics. For example, developing an automatic translation from procedural to declarative style proofs, which are close to informal proofs (one such example is miz3 for HOL Light [1]). Second, suggestion to introduce archives of formal proofs [2] for HOL4, which is an efficient way to maintain large HOL4 scripts. In this way the HOL4 scripts (particularly related to application) can be centralized which are usually available on research groups or individual researchers webpages.

[1] F. Wiedijk, A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving, Logical Methods in Computer Science (8), 2012 [http://arxiv.org/abs/1201.3601]

[2] http://afp.sourceforge.net/

ABSTRACT. Much of HOL's documentation looks and feels old. I propose that we try to modernise the documentation to make it more appealing to, say, masters students who might like to do projects using HOL. I'm thinking that the documentation could be in some new format, e.g. screencasts, a blog, a new well-linked website, wiki or something even better. I hope there will be a fruitful discussion that leads to real improvements.

ABSTRACT. The HOL-to-CakeML translator, which is described in Myreen and Owens's ICFP'12 paper, is a nice self-contained piece of proof-automation. I propose describing its implementation. If the audience is mostly consisting of beginners, this talk can be geared towards a tutorial-style introduction into how proof automation for HOL can be implemented. If, on the other hand, the audience consists mostly of HOL experts, then this talk can serve as a discussion of methods by which proof automation is constructed.

ABSTRACT. I propose briefly talking about the following HOL4 “hidden features”.

1. The function HolKernel.syntax_fns. This function simplifies the task of writing *Syntax files, resulting in more compact code and reducing the likelihood of making mistakes. I’d like to encourage HOL4 developers to make use of this function. I’d
   also like to seek feedback on whether or not it is a good idea to update old *Syntax files.
2. The function EmitTeX.datatype_thm_to_string. This is useful for anyone using EmitML, however it is very easy to overlook because it is located under EmitTeX.
3. There are various useful library functions located under the examples directory, such as l3-machine-code/common/utilsLib and machine-code/hoare-triple/ helperLib.For example, there are the functions: utilsLib.add_datatypes, utilsLib.HYP_CONV_RULE and helperLib.quote_to_strings. This last function has a variant elsewhere, namely l3-machine-code/lib/assemblerLib.quote_ to_strings. It would be good to discuss the issue of finding better homes for some of these functions.
4. The theories numposrep, ASCIInumbers and bitstring. The bit-string theory is relatively new and I propose discussing how it is related to these other two theories, as well as to words theory. I may also discuss some tools bitstringLib.

ABSTRACT. I propose to talk in general about the tensions between different approaches to constructing proofs: maintainability, construction speed, replay speed, readability, etc. and also to highlight a few relatively unknown tactics, packages, and ways of using them: lcsymtacs, match_rename etc., quant heuristics (maybe), writing conversions, using MATCH_MP. I hope to both share and learn tips and tricks for writing proofs effectively.

For another kind of hidden feature, I propose to highlight the issue tracker and other resources that are being used, and could be used more effectively, to improve HOL development. Along these lines, I also propose regular developer workshops.

(Additionally, if there is time, I would propose some longer-term feature requests including some that already appear in the issue tracker, and others such as partial functions, BNF datatypes, logic programming in proof automation, and mechanisms for locale-style development.)

ABSTRACT. Interspersed with our hack sessions on implementing and discussing bugs and new features for HOL4, we will have time for discussion of e.g. future directions for HOL workshops, cool applications and theorem proving ideas, impromptu talks, Q&A, etc.