Open thalerjonathan opened 6 years ago
Totality of agent behaviour can be checked (to a certain extent) This is not unique to dependent types but is nicely supported by Idris. If all functions the agent uses are total then the agent is total which means we have even stronger guarantees about correctness. By totality of a function we understand that it produces an answer in finite time for all possible inputs.
After finished studying the Idris Book and having developed a proper understanding of Dependen Types, investigate where and how dependent types could be of use in my pure functional approach to ABS. I explicitly want to focus on Idris as context of this research.