phd_jasper.bib

@book{klabnik19,
  title     = {The Rust Programming Language},
  author    = {Steve Klabnik and Carol Nichols},
  year      = {2019},
  publisher = {No Starch Press},
  link      = {https://rust-lang.org}
}

@article{moura15,
  title  = {The Lean theorem prover},
  author = {Leonardo de Moura and Soonho Kong and Jeremy Avigad and Floris van Doorn and Jakob von Raumer},
  year   = {2015},
  link   = {https://leanprover.github.io/}
}

@inproceedings{moura08,
  title        = {Z3: An efficient SMT solver},
  author       = {Moura, Leonardo de and Bjørner, Nikolaj},
  booktitle    = {International conference on Tools and Algorithms for the Construction and Analysis of Systems},
  pages        = {337--340},
  year         = {2008},
  organization = {Springer},
  link         = {https://github.com/Z3Prover}
}

@inproceedings{vazou14,
  title     = {Refinement types for Haskell},
  author    = {Vazou, Niki and Seidel, Eric L and Jhala, Ranjit and Vytiniotis, Dimitrios and Peyton-Jones, Simon},
  booktitle = {Proceedings of the 19th ACM SIGPLAN international conference on Functional programming},
  pages     = {269--282},
  year      = {2014},
  link      = {https://ucsd-progsys.github.io/liquidhaskell-blog/}
}

% Paper?
@online{haskell22,
  title   = {Haskell},
  author  = {Haskell.org},
  url     = {https://www.haskell.org/},
  date    = {2022-01-26},
  urldate = {2022-01-26}
}

@misc{xi10,
  title     = {The ATS Programming Language},
  author    = {Xi, Hongwei},
  year      = {2010},
  publisher = {Citeseer},
  link      = {http://www.ats-lang.org/}
}

@online{clippy22,
  title   = {Clippy},
  author  = {Clippy Team},
  url     = {https://github.com/rust-lang/rust-clippy},
  date    = {2022-02-04},
  urldate = {2022-02-04}
}

@online{tolnay22,
  title   = {Cargo Expand},
  author  = {David Tolnay},
  url     = {https://github.com/dtolnay/cargo-expand
             },
  date    = {2022-02-04},
  urldate = {2022-02-04}
}

@online{tutisani22,
  title   = {Why TDD is Faster than Unit Testing},
  author  = {Tengiz Tutisani},
  url     = {https://www.tutisani.com/software-architecture/why-tdd-is-faster-than-unit-testing.html},
  urldate = {2202-02-04}
}

@online{rustdoc22,
  title   = {The rustdoc book},
  author  = {Rust Team},
  url     = {https://doc.rust-lang.org/rustdoc/},
  urldate = {2202-02-04}
}

@online{mdbook22,
  title   = {mdBook Docmentation},
  author  = {Rust Team},
  url     = {https://rust-lang.github.io/mdBook/},
  urldate = {2202-02-04}
}

@article{jung17rustbelt,
  title     = {RustBelt: Securing the foundations of the Rust programming language},
  author    = {Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek},
  journal   = {Proceedings of the ACM on Programming Languages},
  volume    = {2},
  number    = {POPL},
  pages     = {1--34},
  year      = {2017},
  publisher = {ACM New York, NY, USA},
  link      = {https://plv.mpi-sws.org/rustbelt/}
}

@online{emc22,
  title   = {European Metrology Cloud},
  author  = {Physikalisch-Technische Bundesanstalt},
  url     = {metrologycloud.eu},
  date    = {2022-01-26},
  urldate = {2022-01-26}
}

@online{refinement22,
  title   = {Refinement},
  author  = {Brady Dean},
  url     = {https://github.com/2bdkid/refinement},
  date    = {2022-01-26},
  urldate = {2022-01-26}
}

@online{proptest22,
  title   = {Proptest Book},
  author  = {Jason Lingle},
  url     = {https://altsysrq.github.io/proptest-book/},
  date    = {2022-01-26},
  urldate = {2022-01-26}
}

@online{rustproof22,
  title   = {RustProof},
  author  = {Rust-Proof},
  url     = {https://github.com/Rust-Proof/rustproof},
  date    = {2022-01-26},
  urldate = {2022-01-26}
}

@article{flanagan06,
  author  = {Cormac Flanagan and Stephen N. Freund and Aaron Tomb},
  title   = {Hybrid types, invariants, and refinements for imperative objects},
  journal = {FOOL/WOOD},
  volume  = {6},
  year    = {2006},
  link    = {https://users.soe.ucsc.edu/~cormac/papers/fool06.pdf}
}

@article{lehmann2017gradual,
  title     = {Gradual refinement types},
  author    = {Lehmann, Nico and Tanter, {\'E}ric},
  journal   = {ACM SIGPLAN Notices},
  volume    = {52},
  number    = {1},
  pages     = {775--788},
  year      = {2017},
  publisher = {ACM New York, NY, USA},
  link      = {https://pleiad.cl/papers/2017/lehmannTanter-popl2017.pdf}
}

@article{thomas19,
  title        = {A proactive approach to more secure code},
  organization = {Microsoft Security Response Center},
  author       = {Gavin Thomas},
  url          = {https://msrc-blog.microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/},
  date         = {2019-07-16},
  urldate      = {2022-01-25}
}

@article{weiss21,
  author  = {Aaron Weiss and Olek Gierczak and Daniel Patterson and Amal Ahmed},
  title   = {Oxide: The Essence of Rust},
  journal = {arXiv preprint arXiv:1903.00982},
  year    = {2021},
  link    = {https://arxiv.org/pdf/1903.00982.pdf}
}

@article{kan20,
  author  = {Shuanglong Kan and Zhe Chen and Davin Saán and Shang-Wei Lin and Yang Liu},
  title   = {An Executable Operational Semantics for Rust with the Formaliztion of Ownership and Borrowing},
  journal = {arXiv preprint arXiv:1804.07608},
  year    = {2020},
  link    = {https://arxiv.org/pdf/1804.07608.pdf}
}

@mastersthesis{ullrich16,
  author = {Sebastian Ullrich},
  title  = {Simple Verification of Rust Programs via Functional Purification},
  school = {Karlsruhe Institute of Technology},
  year   = {2016},
  link   = {https://pp.ipd.kit.edu/uploads/publikationen/ullrich16masterarbeit.pdf}
}

@mastersthesis{kooi21,
  author = {Xiu Hong Kooi},
  title  = {Refinement Types in Real-World Programming},
  school = {University pf Cambridge},
  year   = 2021,
  link   = {https://kooixiuhong.com/static/media/acs-dissertation.e8569509.pdf}
}

@inproceedings{vekris2016refinement,
  title     = {Refinement types for TypeScript},
  author    = {Vekris, Panagiotis and Cosman, Benjamin and Jhala, Ranjit},
  booktitle = {Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages     = {310--325},
  year      = {2016},
  link      = {https://goto.ucsd.edu/~pvekris/docs/pldi16.pdf}
}

@article{reed15,
  author  = {Eric Reed},
  title   = {Patina: A formalization of the Rust programming language},
  journal = {University of Washington, Department of Computer Science and Engineering, Tech. Rep. UW-CSE-15-03-02},
  pages   = {264},
  year    = {2015},
  link    = {https://dada.cs.washington.edu/research/tr/2015/03/UW-CSE-15-03-02.pdf}
}

@techreport{prusti19,
  author      = {V. Astrauskas and P. Müller and F. Poli and A. J. Summers},
  title       = {Leveraging Rust Types for Modular Specification and Verification},
  institution = {ETH Zurich},
  year        = {2019},
  doi         = {10.3929/ethz-b-000311092}
}

@inproceedings{mueller16,
  author    = {P. Müller and M. Schwerhoff and A. J. Summers},
  title     = {Viper: A Verification Infrastructure for Permission-Based Reasoning},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  editor    = {B. Jobstmann and K. R. M. Leino},
  year      = {2016},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  pages     = {41-62},
  volume    = {9583}
}

@article{rondon08,
  author     = {Partrick M. Rondon and Ming Kawaguci and Ranjit Jhala},
  title      = {Liquid Types},
  doi        = {10.1145/1375581.1375602},
  year       = {2008},
  eventtitle = {PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages      = {159-169}
}

@report{olson16,
  author = {Scott Olson},
  school = {University of Saskatchewan},
  title  = {Miri: An interpreter for Rust’s mid-level intermediate representation},
  url    = {https://solson.me/miri-report.pdf}
}

@online{matsakis18,
  author  = {Niko Matsakis},
  title   = {An alias-based formulation of the borro checker},
  date    = {2018-04-27},
  url     = {https://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/#fnref:covariant},
  urldate = {2022-02-17}
}

@misc{enwiki:1064721744,
  author       = {{Wikipedia contributors}},
  title        = {Datalog --- {Wikipedia}{,} The Free Encyclopedia},
  year         = {2022},
  howpublished = {\url{https://en.wikipedia.org/w/index.php?title=Datalog&oldid=1064721744}},
  note         = {[Online; accessed 17-February-2022]}
}

@article{pearce21,
  title     = {A lightweight formalism for reference lifetimes and borrowing in Rust},
  author    = {Pearce, David J},
  journal   = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume    = {43},
  number    = {1},
  pages     = {1--73},
  year      = {2021},
  publisher = {ACM New York, NY, USA}
}

@inproceedings{matsushita2020rusthorn,
  title     = {RustHorn: CHC-Based Verification for Rust Programs.},
  author    = {Matsushita, Yusuke and Tsukada, Takeshi and Kobayashi, Naoki},
  booktitle = {ESOP},
  pages     = {484--514},
  year      = {2020}
}

@inproceedings{wang2018krust,
  title        = {Krust: A formal executable semantics of rust},
  author       = {Wang, Feng and Song, Fu and Zhang, Min and Zhu, Xiaoran and Zhang, Jun},
  booktitle    = {2018 International Symposium on Theoretical Aspects of Software Engineering (TASE)},
  pages        = {44--51},
  year         = {2018},
  organization = {IEEE}
}

  @misc{enwiki:1071814133,
  author       = {{Wikipedia contributors}},
  title        = {Horn clause --- {Wikipedia}{,} The Free Encyclopedia},
  year         = {2022},
  howpublished = {\url{https://en.wikipedia.org/w/index.php?title=Horn_clause&oldid=1071814133}},
  note         = {[Online; accessed 10-March-2022]}
}

@article{roșu2010kframework,
  title     = {An overview of the K semantic framework},
  author    = {Roșu, Grigore and Șerb{\u{a}}nut{\u{a}}, Traian Florin},
  journal   = {The Journal of Logic and Algebraic Programming},
  volume    = {79},
  number    = {6},
  pages     = {397--434},
  year      = {2010},
  publisher = {Elsevier}
}