Published: 1st May 2020|
|Preface Sam Lindley and Max S. New|
|From Equations to Distinctions: Two Interpretations of Effectful Computations Niels Voorneveld||1|
|Unifying graded and parameterised monads Dominic Orchard, Philip Wadler and Harley Eades III||18|
|Combining predicate transformer semantics for effects: a case study in parsing regular languages Anne Baanen and Wouter Swierstra||39|
|Multi-dimensional Arrays with Levels Artjoms Šinkarovs||57|
|Efficient lambda encodings for Mendler-style coinductive types in Cedille Christopher Jenkins, Aaron Stump and Larry Diehl||72|
This volume contains the proceedings of the Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020). The meeting was originally scheduled to take place in Dublin, Ireland on the 25th of April as a satellite event of the European Joint Conferences on Theory & Practice of Software (ETAPS 2020).
Due to the COVID-19 pandemic, ETAPS 2020, and consequently MSFP 2020, has been postponed to a date yet to be determined.
The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal language semantics to the development of simple and reasonable programs. This year's papers cover a variety of topics ranging from array programming to dependent types to effects.
We are honoured to host the following invited speakers:
Sam Lindley and Max S. New, April 2020
Presheaves are a staple categorical structure, which naturally arises in a wide variety of situations. In the realm of logic, they are often used as a model factory. Indeed, presheaves over some base category will result in a topos, whose contents can be fine-tuned by carefully picking the base category. As computer scientists, though, we have learnt that there are even better logical systems than toposes: dependent type theories! Through the Curry-Howard mirror, they are also full-blown functional programming languages that actually compute.
This begs the following question: is it possible to build the type-theoretic equivalent of presheaves, while retaining the good computational properties of our dependent programming languages? We will see that strikingly enough, presheaves can already be presented as computational objects to some extent, except for the annoying fact that they do not obey the right conversion rules! A proper account of type-theoretic presheaves will require a coming-of-age journey through the world of effectful program semantics, using fine and modern tools such as call-by-push-value, dependent parametricity and strict equality. In the end, we will formulate an alternative presentation of presheaves in type theory, but which is still equivalent to its standard categorical counterpart when viewed from the static world of sets. As an application, we will use them to extend dependent type theory with new effective logical principles.
Too often we design a hardware artifact, we verify it using testing, and in some cases formal verification, and finally we may attribute a semantics to an existing circuit to see if we can understand what it means. For developing high assurance hardware (e.g. crypto circuits, silicon root of trust) this is a very unsatisfactory state of affairs. The difficulties are compounded when we try to somehow transcribe a circuit implementation in a hugely complex hardware description language like Verilog into the logic of a theorem prover.
This talk describes an attempt to do things differently that views the formal specification and verification of hardware as an act of development intertwined with the implementation. Formal specification at the outset is very much used as a way of developing, thinking, and exploring the design space rather than being an after thought for a fait accompli.
Our approach is very much inspired by the Kami project at MIT which is currently being used to develop RISC-V processors at the company SiFive. We instead focus on low level circuits and crypto accelerators and we have developed a different set of abstractions suited for describing and attributing semantics to low level circuit blocks. The approach we take involves recasting the Lava hardware description language originally developed in Haskell as a DSL in the Coq theorem prover. Circuit descriptions are composed using overloaded monadic combinators which are parameterized on the type of values flowing over the wires. For one interpretation we can generate circuit graphs with cycles which represent circuit netlists which can be converted to SystemVerilog hardware description (via Coq's Haskell extraction mechanism). Another interpretation of exactly the same structure yields a model of the circuit behaviour which can be used for formal verification against a formal specification (recurrence equations over streams in our case). We apply this technique to the specification and verification of the circuit blocks that comprise the OpenTitan silicon root of trust specification and reference implementation.