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

Depends on

Cite

× 
@article{NREST-AFP,
  author  = {Maximilian P. L. Haslbeck},
  title   = {NREST: Nondeterministc RESult monad with Time},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/NREST.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest