NREST: Nondeterministc RESult monad with Time

Maximilian P. L. Haslbeck 📧

September 16, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry introduces NREST, a nondeterministc result monad with time, which was spun off a development of a framework for verifying functional correctness and worst-case complexity of algorithms refined down to LLVM, due to Haslbeck and Lammich.

License

BSD License

Topics

Related publications

  • Haslbeck, M. P. L., & Lammich, P. (2022). For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM. ACM Transactions on Programming Languages and Systems, 44(3), 1–36. https://doi.org/10.1145/3486169
  • Haslbeck, M. P. L., & Lammich, P. (2021). For a Few Dollars More. Programming Languages and Systems, 292–319. https://doi.org/10.1007/978-3-030-72019-3_11

Session NREST