Oskar Abrahamsson

11 papers A* 1A 1B 2Journal 6Unranked 1
YearRankTypeTitle / Venue / Authors
2025 J jnl
Candle: A Verified Implementation of HOL Light (Extended Version).
J. Autom. Reason.
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
2025 J jnl
Fast, Verified Computation for HOL ITPs.
J. Autom. Reason.
Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Hrutvik Kanabar, Johannes Åman Pohjola
2023 J jnl
Cakes That Bake Cakes: Dynamic Computation in CakeML.
Proc. ACM Program. Lang.
Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens
2023 B conf
Fast, Verified Computation for Candle.
ITP
Oskar Abrahamsson, Magnus O. Myreen
2023 J jnl
PureCake: A Verified Compiler for a Lazy Functional Language.
Proc. ACM Program. Lang.
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti
2022 B conf
Candle: A Verified Implementation of HOL Light.
ITP
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
2020 J jnl
A verified proof checker for higher-order logic.
J. Log. Algebraic Methods Program.
Oskar Abrahamsson
2020 J jnl
Proof-Producing Synthesis of CakeML from Monadic HOL Functions.
J. Autom. Reason.
Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan
2019 A* conf
Verified compilation on a verified processor.
PLDI
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox
2018 A conf
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.
IJCAR
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish
2017 — conf
Automatically Introducing Tail Recursion in CakeML.
TFP
Oskar Abrahamsson, Magnus O. Myreen