<div dir="ltr"><div>I might be interested in building a Coq/Agda/Twelf model for sure :)<br><br></div>But given that, it is often good to have a interpreted model in a more "normal" programming language as well in my experience. They tend to be more tangible in many cases. Perhaps a Coq extraction will do?<br><br></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Nov 30, 2017 at 4:33 PM Simon  Thompson <<a href="mailto:S.J.Thompson@kent.ac.uk">S.J.Thompson@kent.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><br></div>Once it’s stable would be great to transform the document into something executable (e.g. Erlang, Haskell) or even verifiable (Isabelle, Coq, K-framework) so that there’s a “reference implementation” which can be tested and verified.<div><br></div><div>Simon<br><div><br></div><div></div></div></div><div style="word-wrap:break-word"><div><div><br><div><blockquote type="cite"><div>On 30 Nov 2017, at 15:29, Rickard Green <<a href="mailto:rickard@erlang.org" target="_blank">rickard@erlang.org</a>> wrote:</div><br class="m_2184199600856307101Apple-interchange-newline"><div><div>On 11/30/2017 04:08 PM, Anthony Ramine wrote:<br><blockquote type="cite">Would be nice to rewrite that in HTML, we are in 2017 after all.<br></blockquote><br>No I don't think it would be a good ide to rewrite this in HTML. There might be other options than latex, but I don't see that HTML would be an option. This due to the mathematical formulas in the document.<br><br>There are tools available to produce html from latex which can be integrated in the makefiles which of course would be nice.<br><br>Regards,<br>Rickard<br><br></div></div></blockquote></div><br></div></div></div><div style="word-wrap:break-word"><div><div><div>
<div><span style="font-family:LucidaGrande">Simon Thompson | Professor of Logic and Computation </span><br style="font-family:LucidaGrande"><span style="font-family:LucidaGrande">School of Computing | University of Kent | Canterbury, CT2 7NF, UK</span><br style="font-family:LucidaGrande"><a href="mailto:s.j.thompson@kent.ac.uk" style="font-family:LucidaGrande" target="_blank">s.j.thompson@kent.ac.uk</a><span style="font-family:LucidaGrande"> | M <a href="tel:+44%207986%20085754" value="+447986085754" target="_blank">+44 7986 085754</a> | W </span><a href="http://www.cs.kent.ac.uk/~sjt" style="font-family:LucidaGrande" target="_blank">www.cs.kent.ac.uk/~sjt</a></div>

</div>
<br></div></div></div>_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
</blockquote></div>