[Agda] ASN.1 and type theory

[David Wahlstedt]

Hello,

I wonder if any of you in this list knows anything about ASN.1, and if you
happen to know about are any tools to translate a given ASN.1 specification
into an algebraic datatype(perhaps also with dependent types)?
Or maybe some type theorist have written about ASN.1 anywhere?

Best regards,
David

[Nils Anders Danielsson]

Post by David Wahlstedt
Or maybe some type theorist have written about ASN.1 anywhere?

A quick search led to

https://github.com/bendy/fiat-asn.1,

which is described as "A formally verified ASN.1 compiler using Fiat".

[David Wahlstedt]

Thanks!

Post by Nils Anders Danielsson

Post by David Wahlstedt
Or maybe some type theorist have written about ASN.1 anywhere?

A quick search led to
https://github.com/bendy/fiat-asn.1,
which is described as "A formally verified ASN.1 compiler using Fiat".
--
/NAD