Marko Dimjašević
Computer scientist interested in correct software
Marko Dimjašević is a computer scientist with research interests in type theory and formal methods. He is an engineer at Input Output Hong Kong where he works on formally specifying a blockchain. Marko holds a doctoral degree in computer science from the University of Utah, USA. His dissertation was on automatic software testing. At NASA he performed research and development on software testing and runtime verification techniques for an aircraft collision avoidance system.
Function Totality: Abstraction Tool in Programming
Abstraction is a cornerstone of programming a complex software system. Without it, a complex software system is a complicated software system. In this talk, an important abstraction tool is considered: function totality. It covers termination and productivity. If a supposedly terminating program is not total, it can lead to a program crash or an infinite loop. Furthermore, a non-total program that needs to run forever can end up in a deadlock. This talk covers techniques for achieving function totality.
In this talk, I will provide several code examples in Haskell, Agda and Idris. Through the examples, I will walk the audience through the topic of function totality and what it means for abstraction and composition. I will gradually build up the motivation for program termination and productiveness, which are known as function totality. Finally, I will provide specific instructions on how to write total functions. In this talk I will be presenting known results in computer science.
SlidesVideo ←Back
