On 2018-04-20 17:06, David Wahlstedt wrote: > 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