[Hol-info] Postdoc Positions at KTH and Chalmers on Cyber-Physical Systems (with CakeML)

We are looking to employ postdocs, one at KTH and one at Chalmers, to conduct research in a joint expedition project titled: High-Confidence Formal Verification of Real Cyber-Physical Systems: from Models to Machine Code The overall goal of this project is to develop new theoretical

[Hol-info] Element assignment in structures

The following data structure is defined in HOL4. val _ = Datatype ` my = <| r: num; b: num; dis: real |>`; Given a mylist(:my list), if a

Re: [Hol-info] (no subject)

Where is this code from? It looks like an exam question. On Thu, 20 Dec 2018 06:24 幻＠未来 <849678...@qq.com wrote: > > Here is the following code > datatype temp = > C of real > | F of real; > fun temp_to_f t = > case t of >C x => x * (9.0 / 5.0) +

Re: [Hol-info] (no subject)

Hi, this is not an HOL question any more, and now you should learn some Standard ML first. Maybe the following book is a good start: Harper, R.: Programming in Standard ML. http://www.cs.cmu.edu/~rwh/isml/book.pdf I??m sure the answer of