The aim of this group is to explore the use of new type systems, in both functional and non-functional languages, to create efficient, problem solving systems that work reliably and can be easily maintained.
The inspiration for starting the group is 'Type-Driven Development with Idris' by Edwin Brady. In that book Brady uses Idris to demonstrate how dependent type systems can be used to help a programmer write working programs.
Some ideas for the group:
* Provide a friendly, welcoming environment for people to learn about ideas in type theory and software engineering. Especially for those who are completely new to them.
* A showcase for people to demo how they've used type theory in practical projects.
* Uses of type-driven development in languages that are not purely functional (e.g Swift)
## Chapter 13 - Coinduction
We are planning on discussing sections 13.5 through 13.7 of the Coq'Art book. Doing the exercises is recommended, but not required.
Read [Coq in a Hurry](https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf) and then don't hesitate to join the sessions. It might be intimidating, but you will pick up a lot from just watching and asking questions. We know it is a tough journey to learn Coq and we would prefer to help where we can.
In May last year we finished reading 'The Little Typer' by Dan Friedman and David Christiansen. We all enjoyed learning about dependent types so much that we decided to continue.
This time we'll be learning about how to use dependent types to write programs in Coq. Coq is a formal proof management system that has been used in industrial applications and formal mathematics.