This abstract presents […] an high-level specification language with important features as channel-over-channel passing, secret channels, and deadlock-freedom, that aims at providing for correctness-by-construction, and is supported by a fully automated tool that infers the types of well-behaved specifications, and generates executable Go code.

Talk: http://ctp.di.fct.unl.pt/~mgiunti/inforum19-talk.pdf Code: https://github.com/marcogiunti/gopi