This page provides a few pointers to the interactions of the EUTypes community with non-academic partners:
- Climate impact research using the Agda proof assistant.
- Keiko Nakata works at SAP SE and she leads WG4. Her team uses the Scala and OCaml programming languages, leveraging their latest language features to develop innovative architectures for applications that are deployed in production. The action held multiple in-person meetings where a key objective was to bring practitioners in touch with key players in the academic world. Along with Ms. Nakata, some of the core developers of the aforementioned languages attended those meetings and exchanged important insights in obstacles and opportunities for industrial adaptation and the mid-term perspectives for future language evolution.
- EUTypes had a satellite event at Lambda Days 2019.
- Michael Soegtrop, at Intel Corporation uses the Coq proof assistant to implement advanced numerical algorithms for adaptive / self adjusting RF circuits.
- Nomadic Labs is funding, or considers funding, several projects related to the Coq proof assistant such as SMTCoq. They announce positions here.
- Mitsubishi Research Center Europe (MERCE) funds the PhD of Enzo Crance co-supervised by Assia Mahboubi (Inria) and Denis Cousineau (MERCE), on enhancing automation for Coq.
- ANSSI, the National Cybersecurity Agency of France has funded the PhD (Specifying and Verifying Hardware-based Security Enforcement Mechanisms) of Thomas Letan, now hired as engineer at ANSSI. He has published several papers about the verification in Coq of programs with effects and effect handlers.
- Conor McBride, Fredrik Nordvall Forsberg and Neil Ghani has started a project on Trusted Systems with the NPL Data Science group (https://www.npl.co.uk/data-science). NPL is the UK's national institute for Measurement Science, and the aim of the project is to use dependent types to enable NPL to gain similar levels of trust in software that they currently have in their processes for physical measurements.
- Statebox (https://statebox.org/) is a Dutch company that are building a formally verified process language using the Idris language. Fredrik Nordvall Forsberg is helping them design a datatype description language to be used when transferring data to and from the Statebox process language.
