1030 

  1031 

  1032 @inproceedings{atkey2010amortised,

  1033   title={Amortised resource analysis with separation logic},

  1034   author={Atkey, Robert},

  1035   booktitle={European Symposium on Programming},

  1036   pages={85--103},

  1037   year={2010},

  1038   organization={Springer}

  1039 }

  1040 

  1041 %10.1007/978-3-319-89884-1_19,

  1042 

  1043 @InProceedings{bigOImperative, 

  1044 author="Gu{\'e}neau, Arma{\"e}l

  1045 and Chargu{\'e}raud, Arthur

  1046 and Pottier, Fran{\c{c}}ois",

  1047 editor="Ahmed, Amal",

  1048 title="A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification",

  1049 booktitle="Programming Languages and Systems",

  1050 year="2018",

  1051 publisher="Springer International Publishing",

  1052 address="Cham",

  1053 pages="533--560",

  1054 abstract="We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.",

  1055 isbn="978-3-319-89884-1"

  1056 }

  1057 %@article{10.1145/640128.604148,

  1058 %author = {Hofmann, Martin and Jost, Steffen},

  1059 %title = {Static Prediction of Heap Space Usage for First-Order Functional Programs},

  1060 %year = {2003},

  1061 %issue_date = {January 2003},

  1062 %publisher = {Association for Computing Machinery},

  1063 %address = {New York, NY, USA},

  1064 %volume = {38},

  1065 %number = {1},

  1066 %issn = {0362-1340},

  1067 %url = {https://doi.org/10.1145/640128.604148},

  1068 %doi = {10.1145/640128.604148},

  1069 %abstract = {We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs.The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort.The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system.We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.},

  1070 %journal = {SIGPLAN Not.},

  1071 %month = {jan},

  1072 %pages = {185–197},

  1073 %numpages = {13},

  1074 %keywords = {heap, functional programming, program analysis, resources, garbage collection}

  1075 %}

  1076 %

  1077 %@inproceedings{10.1145/604131.604148,

  1078 %author = {Hofmann, Martin and Jost, Steffen},

  1079 %title = {Static Prediction of Heap Space Usage for First-Order Functional Programs},

  1080 %year = {2003},

  1081 %isbn = {1581136285},

  1082 %publisher = {Association for Computing Machinery},

  1083 %address = {New York, NY, USA},

  1084 %url = {https://doi.org/10.1145/604131.604148},

  1085 %doi = {10.1145/604131.604148},

  1086 %abstract = {We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs.The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort.The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system.We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.},

  1087 %booktitle = {Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},

  1088 %pages = {185–197},

  1089 %numpages = {13},

  1090 %keywords = {resources, heap, garbage collection, program analysis, functional programming},

  1091 %location = {New Orleans, Louisiana, USA},

  1092 %series = {POPL '03}

  1093 %}

  1094 

  1095