Publications

A list of my publications.

Attributes

Graph
Supertypes: class Object

trait Matchable

class Any
Self type: Publications.type

Members list

Type members

Classlikes

Verified Inlining and Specialisation for PureCake

Inlining is a crucial optimisation when compiling functional programming languages. This paper describes how we have implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like (purely functional, lazy) programming language. A novel aspect of our formalisation is that we justify inlining by pushing and pulling -bindings. All of our work has been mechanised in the HOL4 interactive theorem prover.

Attributes

Authors:: Hrutvik Kanabar, Kacper Korban, Magnus O Myreen
See also: https://scholar.google.com/citations?view_op=view_citation&hl=pl&user=eTmlLwEAAAAJ&citation_for_view=eTmlLwEAAAAJ:d1gkVwhDpl0C
Since: ESOP 2024
Supertypes: class Object

trait Matchable

class Any

In this article

Generated with