This presentation discusses how functional programming and dependent types can improve trustworthiness of software in measurement science.
Speakers
- Keith Lines
- Andre Videla
Agenda
5:15pm - Networking for all attendees
6:00pm - Seminar
7:00pm - Q&A
7:30pm - Networking for all attendees
8:30pm - End
Synopsis
This presentation will summarise work undertaken by the Data Science Department of the National Physical Laboratory and the Mathematically Structured Programming Group of the University of Strathclyde to investigate how functional programming and dependent types could increase trustworthiness of software used in measurement science (metrology).
Code written in a functional language can provide a more self-evidently correct implementation of an underlying mathematical model than code written in a more traditional imperative language. Dependent types can provide helpful contextual information. For example, a matrix containing measurement values could use a column index to determine the unit of measurement associated with the values held in that column. Such features are built into the type system itself, no extra coding is required. An important challenge was to determine how to make such topics accessible to metrologists, a technically knowledgeable audience but not one consisting of specialists in theoretical computer science. Case studies will demonstrate advantages that functional programming languages, including those that provide dependent types, can provide when compared to more commonly used languages such as Python.
About the speaker
Keith Lines works in the Data Science department of the National Physical Laboratory. applies experience gained in over 34 years of working with NPL's scientists, administrators and support staff to help ensure that NPL activities in software development continue to meet the requirements of NPL's ISO 9001 and TickITplus certifications. Formal aspects of computing have been an interest since he was a student at the University of Kent in the mid-1980s. He is a member of the BCS.
André Videla is a researcher at Glaive, a Glasgow-based independent research group focused on AI safety. He also works on programming languages with dependent types and helps maintain the Idris programming language. His theoretical work surrounds the category of containers, also known as polynomial functors, and their morphisms, for which he studied their application in modern software engineering in areas such as compiler architecture, web servers, and theorem provers. He likes taking concepts such as type theory and category theory and deploying their application in software engineering and programming.
Our events are for adults aged 16 years and over.
BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today
If you are attending in person, please familiarise yourself with the Visitor Instructions for the BCS London Office.
Please note: if you have any accessibility needs, please let us know via groups@bcs.uk and we’ll work with you to make suitable arrangements.
For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.
This event is brought to you by: FACS (Formal Aspects of Computing Science) group
