[msp-interest] [MSP101] André Videla: Pipelining and dependent types (LT412, 3pm Mon 27-Jan)

[Dilsat Yuksel]

Hi all,

On Monday, the MSP101 talk will be given by André Videla (MSP). See the details of the talk below.

Best,
Dilsat

**********************************************************************

Date: Monday, 27 January at 15:00

Room: LT412, Livingstone Tower

Zoom link: https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1

Speaker: André Videla

Title: Pipelining and dependent types

Abstract: Pipelining is a crude CPU optimisation to speed up execution of sequential programs. By allowing the manipulation of types as values, dependent types enable new abstractions to manipulate large-scale of software based on sequential computation inspired by CPU pipelining. I will show how to define pipelines, sequential programs that cannot easily be parallelised using a list of types as a specification. Given this list of type, the implementation of a pipeline is given by the functions between each type. This pipeline abstraction can be generalised to categories such that the pipeline is made up of objects and its implementation is given by the morphisms between them. This enable the use of kleisli morphisms for effectful programs. The pipeline can be further abstracted over graded categories enabling automatic composition of errors. Finally, I will show how to use dependent pipelines to allow composition of programs with type-dependency. An architecture particularly useful for single-pass compilers with well-scoped and well-typed implementations.

**********************************************************************

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20250124/6b89fc13/attachment.html