Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New paper: A Compiled Implementation of Normal...

Email Gateway (Aug 18 2022 at 11:25):

From: Tobias Nipkow <nipkow@in.tum.de>
We would like to announce a new paper (and Isabelle formalization):

A Compiled Implementation of Normalization by Evaluation
Klaus Aehlig, Florian Haftmann, Tobias Nipkow

We present a novel compiled approach to Normalization by Evaluation
(NBE) for ML-like languages. It supports efficient normalization of open
lambda-terms w.r.t. beta-reduction and rewrite rules. We have
implemented NBE and show both a detailed formal model of our
implementation and its verification in Isabelle. Finally we discuss how
NBE is turned into a proof rule in Isabelle.

http://www.in.tum.de/~nipkow/pubs/nbe.html

Comments are welcome.

Tobias

Last updated: May 03 2024 at 12:27 UTC