[erlang-questions] Erlang Language Specification

[Jesper Louis Andersen]

I might be interested in building a Coq/Agda/Twelf model for sure :)

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?


On Thu, Nov 30, 2017 at 4:33 PM Simon Thompson <S.J.Thompson@REDACTED>
wrote:

>
> 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.
>
> Simon
>
>
> On 30 Nov 2017, at 15:29, Rickard Green <rickard@REDACTED> wrote:
>
> On 11/30/2017 04:08 PM, Anthony Ramine wrote:
>
> Would be nice to rewrite that in HTML, we are in 2017 after all.
>
>
> 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.
>
> There are tools available to produce html from latex which can be
> integrated in the makefiles which of course would be nice.
>
> Regards,
> Rickard
>
>
> Simon Thompson | Professor of Logic and Computation
> School of Computing | University of Kent | Canterbury, CT2 7NF, UK
> s.j.thompson@REDACTED | M +44 7986 085754 <+44%207986%20085754> | W
> www.cs.kent.ac.uk/~sjt
>
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20171130/bbff6100/attachment.htm>