# Changeset 3651

Ignore:
Timestamp:
Mar 14, 2017, 11:14:29 AM (12 months ago)
Message:

more work on conclusions and related work, bibliography growing to gigantic proportions

Location:
Papers/jar-cerco-2017
Files:
2 edited

Unmodified
Added
Removed
• ## Papers/jar-cerco-2017/cerco.bib

 r3650 address = {New York, NY, USA}, keywords = {CompCert, Compositional compiler verification, separate compilation}, } @Inbook{Atkey2010, author="Atkey, Robert", editor="Gordon, Andrew D.", title="Amortised Resource Analysis with Separation Logic", bookTitle="Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings", year="2010", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="85--103", isbn="978-3-642-11957-6", doi="10.1007/978-3-642-11957-6_6", url="http://dx.doi.org/10.1007/978-3-642-11957-6_6" } @Inbook{Aspinall2010, author="Aspinall, David and Atkey, Robert and MacKenzie, Kenneth and Sannella, Donald", editor="Wirsing, Martin and Hofmann, Martin and Rauschmayer, Axel", title="Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode", bookTitle="Trustworthly Global Computing: 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers", year="2010", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="1--22", isbn="978-3-642-15640-3", doi="10.1007/978-3-642-15640-3_1", url="http://dx.doi.org/10.1007/978-3-642-15640-3_1" } @article{Salvucci201627, title = "Memory Consumption Analysis for a Functional and Imperative Language ", journal = "Electronic Notes in Theoretical Computer Science ", volume = "330", number = "", pages = "27 - 46", year = "2016", note = "\{RAC\} 2016 - Resource Aware Computing ", issn = "1571-0661", doi = "http://dx.doi.org/10.1016/j.entcs.2016.12.013", url = "http://www.sciencedirect.com/science/article/pii/S1571066116301207", author = "Jérémie Salvucci and Emmanuel Chailloux", keywords = "ML", keywords = "regions", keywords = "static analysis", keywords = "memory analysis ", abstract = "Abstract The omnipresence of resource-constrained embedded systems makes them critical components. Programmers have to provide strong guarantees about their runtime behavior to make them reliable. Among these, giving an upper bound of live memory at runtime is mandatory to prevent heap overflows from happening. The paper proposes a semi-automatic technique to infer the space complexity of ML-like programs with explicit region management. It aims at combining existing formalisms to obtain the space complexity of imperative and purely functional programs in a consistent framework. " } @Inbook{Hoffmann2015, author="Hoffmann, Jan and Shao, Zhong", editor="Vitek, Jan", title="Automatic Static Cost Analysis for Parallel Programs", bookTitle="Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings", year="2015", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="132--157", isbn="978-3-662-46669-8", doi="10.1007/978-3-662-46669-8_6", url="http://dx.doi.org/10.1007/978-3-662-46669-8_6" } @inproceedings{HAH12, author    = {Jan Hoffmann and Klaus Aehlig and Martin Hofmann}, title     = {{Resource Aware ML}}, booktitle = {{24rd International Conference on Computer Aided Verification (CAV'12)}}, publisher = {Springer}, series    = {Lecture Notes in Computer Science}, volume    = {7358}, pages     = {781-786}, year      = {2012} } address = {New York, NY, USA}, keywords = {compiler verification, interactive proof assistants}, } } @Article{Albert2011, author="Albert, Elvira and Arenas, Puri and Genaim, Samir and Puebla, Germ{\'a}n", title="Closed-Form Upper Bounds in Static Cost Analysis", journal="Journal of Automated Reasoning", year="2011", volume="46", number="2", pages="161--203", abstract="The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, the analysis first produces cost relations (CRs), i.e., recursive equations which capture the cost of the program in terms of the size of its input data. Second, CRs are converted into closed-form, i.e., without recurrences. Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has been comparatively less studied. This article presents, to our knowledge, the first practical framework for the generation of closed-form upper bounds for CRs which (1) is fully automatic, (2) can handle the distinctive features of CRs, originating from cost analysis of realistic programming languages, (3) is not restricted to simple complexity classes, and (4) produces reasonably accurate solutions. A key idea in our approach is to view CRs as programs, which allows applying semantic-based static analyses and transformations to bound them, namely our method is based on the inference of ranking functions and loop invariants and on the use of partial evaluation.", issn="1573-0670", doi="10.1007/s10817-010-9174-1", url="http://dx.doi.org/10.1007/s10817-010-9174-1" } @article{ALBERT200767, title = "Experiments in Cost Analysis of Java Bytecode", journal = "Electronic Notes in Theoretical Computer Science", volume = "190", number = "1", pages = "67 - 83", year = "2007", note = "", issn = "1571-0661", doi = "http://dx.doi.org/10.1016/j.entcs.2007.02.061", url = "http://www.sciencedirect.com/science/article/pii/S1571066107005294", author = "E. Albert and P. Arenas and S. Genaim and G. Puebla and D. Zanardini", keywords = "Cost analysis", keywords = "Java bytecode", keywords = "cost relations", keywords = "recurrence equations", keywords = "complexity" } @article{Wang:2014:CVM:2714064.2660201, doi = {10.1007/978-3-642-00590-9_14} } @Inbook{Chalin2006, author="Chalin, Patrice and Kiniry, Joseph R. and Leavens, Gary T. and Poll, Erik", editor="de Boer, Frank S. and Bonsangue, Marcello M. and Graf, Susanne and de Roever, Willem-Paul", title="Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2", bookTitle="Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures", year="2006", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="342--363", isbn="978-3-540-36750-5", doi="10.1007/11804192_16", url="http://dx.doi.org/10.1007/11804192_16" } @book{KeYBook2016, title = {Deductive Software Verification - The KeY Book - From Theory to Practice}, editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"{a}}hnle and Peter H. Schmitt and Mattias Ulbrich}, url = {http://dx.doi.org/10.1007/978-3-319-49812-6}, doi = {10.1007/978-3-319-49812-6}, isbn = {978-3-319-49811-9}, year = {2016}, date = {2016-12-16}, volume = {10001}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, keywords = {}, pubstate = {published}, tppubtype = {book} } @Inbook{Montenegro2010a, author="Montenegro, Manuel and Pe{\~{n}}a, Ricardo and Segura, Clara", editor="van Eekelen, Marko and Shkaravska, Olha", title="A Space Consumption Analysis by Abstract Interpretation", bookTitle="Foundational and Practical Aspects of Resource Analysis: First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers", year="2010", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="34--50", isbn="978-3-642-15331-0", doi="10.1007/978-3-642-15331-0_3", url="http://dx.doi.org/10.1007/978-3-642-15331-0_3" } @Inbook{Montenegro2010, author="Montenegro, Manuel and Pe{\~{n}}a, Ricardo and Segura, Clara", editor="Escobar, Santiago", title="A Simple Region Inference Algorithm for a First-Order Functional Language", bookTitle="Functional and Constraint Logic Programming: 18th International Workshop, WFLP 2009, Brasilia, Brazil, June 28, 2009, Revised Selected Papers", year="2010", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="145--161", isbn="978-3-642-11999-6", doi="10.1007/978-3-642-11999-6_10", url="http://dx.doi.org/10.1007/978-3-642-11999-6_10" } @Inbook{deDios2011, author="de Dios, Javier and Pe{\~{n}}a, Ricardo", editor="Butler, Michael and Schulte, Wolfram", title="Certification of Safe Polynomial Memory Bounds", bookTitle="FM 2011: Formal Methods: 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings", year="2011", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="184--199", isbn="978-3-642-21437-0", doi="10.1007/978-3-642-21437-0_16", url="http://dx.doi.org/10.1007/978-3-642-21437-0_16" } @Inbook{Albert2012, author="Albert, Elvira and Bubel, Richard and Genaim, Samir and H{\"a}hnle, Reiner and Rom{\'a}n-D{\'i}ez, Guillermo", editor="de Lara, Juan and Zisman, Andrea", title="Verified Resource Guarantees for Heap Manipulating Programs", bookTitle="Fundamental Approaches to Software Engineering: 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings", year="2012", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="130--145", isbn="978-3-642-28872-2", doi="10.1007/978-3-642-28872-2_10", url="http://dx.doi.org/10.1007/978-3-642-28872-2_10" } @Inbook{Nipkow2015, author="Nipkow, Tobias", editor="Urban, Christian and Zhang, Xingyuan", title="Amortized Complexity Verified", bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings", year="2015", publisher="Springer International Publishing", address="Cham", pages="310--324", isbn="978-3-319-22102-1", doi="10.1007/978-3-319-22102-1_21", url="http://dx.doi.org/10.1007/978-3-319-22102-1_21" } @article{Hoffmann:2012:MAR:2362389.2362393, author = {Hoffmann, Jan and Aehlig, Klaus and Hofmann, Martin}, title = {Multivariate Amortized Resource Analysis}, journal = {ACM Trans. Program. Lang. Syst.}, issue_date = {October 2012}, volume = {34}, number = {3}, month = nov, year = {2012}, issn = {0164-0925}, pages = {14:1--14:62}, articleno = {14}, numpages = {62}, url = {http://doi.acm.org/10.1145/2362389.2362393}, doi = {10.1145/2362389.2362393}, acmid = {2362393}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Amortized analysis, functional programming, quantitative analysis, resource consumption, static analysis}, } @Inbook{Chargueraud2015, author="Chargu{\'e}raud, Arthur and Pottier, Fran{\c{c}}ois", editor="Urban, Christian and Zhang, Xingyuan", title="Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation", bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings", year="2015", publisher="Springer International Publishing", address="Cham", pages="137--153", isbn="978-3-319-22102-1", doi="10.1007/978-3-319-22102-1_9", url="http://dx.doi.org/10.1007/978-3-319-22102-1_9" } @Inbook{Teller2002, author="Teller, David and Zimmer, Pascal and Hirschkoff, Daniel", editor="Brim, Lubo{\v{s}} and K{\v{r}}et{\'i}nsk{\'y}, Mojm{\'i}r and Ku{\v{c}}era, Anton{\'i}n and Jan{\v{c}}ar, Petr", title="Using Ambients to Control Resources*                  ", bookTitle="CONCUR 2002 --- Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20--23, 2002 Proceedings", year="2002", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="288--303", isbn="978-3-540-45694-0", doi="10.1007/3-540-45694-5_20", url="http://dx.doi.org/10.1007/3-540-45694-5_20" } @article{DBLP:journals/jfp/0002S15, author    = {Jan Hoffmann and Zhong Shao}, title     = {Type-based amortized resource analysis with integers and arrays}, journal   = {J. Funct. Program.}, volume    = {25}, year      = {2015}, url       = {http://dx.doi.org/10.1017/S0956796815000192}, doi       = {10.1017/S0956796815000192}, timestamp = {Tue, 26 Jan 2016 16:08:20 +0100}, biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jfp/0002S15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @Inbook{Barbanera2003, author="Barbanera, Franco and Bugliesi, Michele and Dezani-Ciancaglini, Mariangiola and Sassone, Vladimiro", editor="Saraswat, Vijay A.", title="A Calculus of Bounded Capacities", bookTitle="Advances in Computing Science -- ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation: 8th Asian Computing Science Conference, Mumbai, India, December 10-12, 2003. Proceedings", year="2003", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="205--223", isbn="978-3-540-40965-6", doi="10.1007/978-3-540-40965-6_14", url="http://dx.doi.org/10.1007/978-3-540-40965-6_14" } @article{Danielsson:2008:LST:1328897.1328457, author = {Danielsson, Nils Anders}, title = {Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures}, journal = {SIGPLAN Not.}, issue_date = {January 2008}, volume = {43}, number = {1}, month = jan, year = {2008}, issn = {0362-1340}, pages = {133--144}, numpages = {12}, url = {http://doi.acm.org/10.1145/1328897.1328457}, doi = {10.1145/1328897.1328457}, acmid = {1328457}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {amortised time complexity, dependent types, lazy evaluation, purely functional data structures}, } @inproceedings{Crary:2000:RBC:325694.325716, author = {Crary, Karl and Weirich, Stephnie}, title = {Resource Bound Certification}, booktitle = {Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, series = {POPL '00}, year = {2000}, isbn = {1-58113-125-9}, location = {Boston, MA, USA}, pages = {184--198}, numpages = {15}, url = {http://doi.acm.org/10.1145/325694.325716}, doi = {10.1145/325694.325716}, acmid = {325716}, publisher = {ACM}, address = {New York, NY, USA}, } @Inbook{McCarthy2016, author="McCarthy, Jay and Fetscher, Burke and New, Max and Feltey, Daniel and Findler, Robert Bruce", editor="Kiselyov, Oleg and King, Andy", title="A Coq Library for Internal Verification of Running-Times", bookTitle="Functional and Logic Programming: 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings", year="2016", publisher="Springer International Publishing", address="Cham", pages="144--162", isbn="978-3-319-29604-3", doi="10.1007/978-3-319-29604-3_10", url="http://dx.doi.org/10.1007/978-3-319-29604-3_10" } @inproceedings { chan-ngo-verifying-2017, title = {Verifying and Synthesizing Constant-Resource Implementations with Types}, author = {Van Chan Ngo and Mario Dehesa-Azuara and Matthew Fredrikson and Jan Hoffmann}, booktitle = {Proceedings of the {IEEE} Symposium on Security and Privacy}, year = {2017}, note = {to appear} } @Inbook{Brady2006, author="Brady, Edwin and Hammond, Kevin", editor="Butterfield, Andrew and Grelck, Clemens and Huch, Frank", title="A Dependently Typed Framework for Static Analysis of Program Execution Costs", bookTitle="Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers", year="2006", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="74--90", isbn="978-3-540-69175-4", doi="10.1007/11964681_5", url="http://dx.doi.org/10.1007/11964681_5" } @inproceedings{Danner:2013:SCA:2428116.2428123, author = {Danner, Norman and Paykin, Jennifer and Royer, James S.}, title = {A Static Cost Analysis for a Higher-order Language}, booktitle = {Proceedings of the 7th Workshop on Programming Languages Meets Program Verification}, series = {PLPV '13}, year = {2013}, isbn = {978-1-4503-1860-0}, location = {Rome, Italy}, pages = {25--34}, numpages = {10}, url = {http://doi.acm.org/10.1145/2428116.2428123}, doi = {10.1145/2428116.2428123}, acmid = {2428123}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {automated theorem proving, certified bounds, higher-order complexity}, } @inproceedings{Reynolds:2002:SLL:645683.664578, author = {Reynolds, John C.}, title = {Separation Logic: A Logic for Shared Mutable Data Structures}, booktitle = {Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science}, series = {LICS '02}, year = {2002}, isbn = {0-7695-1483-9}, pages = {55--74}, numpages = {20}, url = {http://dl.acm.org/citation.cfm?id=645683.664578}, acmid = {664578}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, } @article{ASPINALL2007411,
• ## Papers/jar-cerco-2017/conclusions.tex

 r3650 Abstract Interpretation may also be used to derive upper bounds for stack usage (e.g.~\cite{Regehr:2005:ESO:1113830.1113833}), and Abstract Interpretation tools for predicting stack space usage, for example the StackAnalyzer tool~\cite{stackanalyzer}, are also commercially available. \paragraph{Type- and program logic-based analyses} \paragraph{High-level approaches} Resource Aware ML (RAML) is a first-order statically typed functional programming language~\cite{Hoffmann11,HAH12Toplas,HoffHof10}. The RAML type system is able to derive polynomial resource bounds from first-order functional programs, using a variant of the potential method'. This approach was first pioneered by Hoffman and Jost for amortized, linear bounds on resource consumption~\cite{DBLP:conf/esop/HofmannJ06}, who focussed on predicting heap-space usage. Campbell also used a variant of this approach to predict stack space usage~\cite{bac-thesis08,bac-giveback08,bac-esop09}. Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}. Here, a fragment of Linear Logic, or some other substructural logic, is taken as the type-language of a programming language, with a provable guarantee that typeable terms normalise to a value in some bounded (e.g. polynomial in the size of the term) number of reduction steps. Note that complained to the concrete complexity measures dealt with in this work, bounding reduction steps is rather coarse-grained: one reduction step in the calculus may decompose into some non-constant number of primitive machine operations, when executed on physical hardware. Indeed, the focus of Implicit Computational Complexity is not to capture \emph{concrete} resource usage of programs, but to provide a type-theoretic interpretation of complexity classes. Several program logics for reasoning about a program's resource consumption have been investigated in the literature. Aspinall et al. developed a program logic for a subset of the Java Virtual Machine's instruction set, capable of establishing resource bounds on JVM programs~\cite{ASPINALL2007411}. The soundness of the logic was formally verified in Isabelle/HOL. Along similar lines, Carbonneaux et al. developed a quantitative Hoare logic' for reasoning about stack space usage of CompCert C programs~\cite{DBLP:conf/pldi/Carbonneaux0RS14}. The soundness of the logic was also formally verified, using the Coq proof assistant. This work will be further discussed below. \subsubsection{High-level approaches} \paragraph{Compiler-based cost-model lifting} Perhaps the most similar piece of work to our own is the recent work by Carbonneaux \emph{et al}~\cite{DBLP:conf/pldi/Carbonneaux0RS14}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C source-level. Perhaps the most closely related piece of work to our own is the recent work by Carbonneaux \emph{et al}~\cite{DBLP:conf/pldi/Carbonneaux0RS14}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C source-level. Like CerCo, this work was verified within a theorem prover---in this case Coq, rather than Matita. Though Carbonneaux \emph{et al} were working entirely independently of the project described herein\footnote{Personal communication with Carbonneaux and Hoffmann}, the two pieces of work share some remarkable similarities, with both projects developing an analogue of the structured trace' data structure described earlier in this paper in order to facilitate the verification of the lifting. Carbonneaux \emph{at al} lift their model from the assembly generated by the CompCert compiler; we must go further, to the level of machine code, in order to lift our timing cost model, necessitating the development of a verified assembler. Nevertheless, despite these differences, the two projects are clearly closely related. Another closely related piece of work to our own is COSTA~\cite{Albert2012}, a heap resource bound static analysis system for the Java programming language, building on previous work investigating cost models for Java bytecode programs~\cite{ALBERT200767}. COSTA is able to produce parametric heap resource bounds for a given Java program, which are made manifest as Java Modelling Language (JML)~\cite{Chalin2006} assertions, inserted into the Java source file. Coupled with the KeY symbolic reasoning/automated reasoning system~\cite{KeYBook2016}, these assertions may be automatically verified, obtaining trustworthy upper bounds on a Java program's dynamic heap space usage at runtime. Other work has explored the use of Computer Algebra Software, such as the Mathematica system, for deriving closed-form upper-bounds of a program's resource usage~\cite{Albert2011}. Previous works have researched various static analyses of time- and space-usage of programs written in a simple functional programming language with regions, called Safe~\cite{Montenegro2010,Montenegro2010a}. One such analysis was verified in Isabelle/HOL~\cite{deDios2011}. The use of types to bound, or program logics to reason about, a program's resource usage have also been extensively investigated in previous work. Resource Aware ML (RAML) is a first-order statically typed functional programming language~\cite{Hoffmann11,HAH12Toplas,HoffHof10,HAH12,DBLP:journals/jfp/0002S15}. The RAML type system is able to derive polynomial resource bounds from first-order functional programs, using a variant of the potential method'. This approach was first pioneered by Hoffman and Jost for amortized, linear bounds on resource consumption~\cite{DBLP:conf/esop/HofmannJ06}, who focussed on predicting heap-space usage. Campbell also used a variant of this approach to predict stack space usage~\cite{bac-thesis08,bac-giveback08,bac-esop09}, whilst Atkey extended the approach to imperative languages~\cite{Atkey2010}, using ideas from Separation Logic~\cite{Reynolds:2002:SLL:645683.664578}. Recent work has extended this approach to include more features of the core programming language~\cite{Hoffmann2015}, improving the resource analysis~\cite{Hoffmann:2012:MAR:2362389.2362393}, and to apply extensions of the technique to case studies, demonstrating that cryptographic code is free from side-channel attacks~\cite{chan-ngo-verifying-2017}. In related work, Salvucci and Chailloux~\cite{Salvucci201627} used a static type and effect system to bound runtime heap usage of an impure functional programming language, similar to ML. Domain-specific type systems and calculi of mobile processes, for bounding agents in a distributed setting, have also been investigated~\cite{Barbanera2003,Teller2002}. Brady and Hammond also investigated a dependent type system extended with features for bounding a program's dynamic resource usage~\cite{Brady2006}. Similar ideas had previously been investigated by Crary and Weirich~\cite{Crary:2000:RBC:325694.325716}. Libraries within dependently-typed languages, such as Coq~\cite{McCarthy2016} and Agda~\cite{Danielsson:2008:LST:1328897.1328457}, have also been written for reasoning about the complexity of algorithms written in the language. One-off machine-checked verifications of the algorithmic complexity of various data structure implementations, and operations over them, have also been investigated (e.g.~\cite{Chargueraud2015,Nipkow2015}). Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}. Here, a fragment of Linear Logic, or some other substructural logic, is taken as the language of types of some calculus, with a provable guarantee that typeable terms of the calculus normalise to a value in some bounded (e.g. polynomial in the size of the term) number of reduction steps. Note that compared to the concrete complexity measures dealt with in this work, bounding reduction steps is rather coarse-grained: one reduction step in the calculus may decompose into some non-constant number of primitive machine operations, when executed on physical hardware. Indeed, the focus of Implicit Computational Complexity is not to capture \emph{concrete} resource usage of programs, but to provide a type-theoretic interpretation of complexity classes. A formalisation of a cost semantics for System T using ideas from Implicit Computational Complexity was formalised in Coq~\cite{Danner:2013:SCA:2428116.2428123}. Several program logics for reasoning about a program's resource consumption have been investigated in the literature. Aspinall et al. developed a program logic for a subset of the Java Virtual Machine's instruction set, capable of establishing resource bounds on JVM programs~\cite{ASPINALL2007411}, similar in spirit to the `quantitative Hoare logic' mentioned above. The soundness of the logic was formally verified in Isabelle/HOL. Another program logic for reasoning about Java resource usage, based on ideas taken from Separation Logic, was also developed by Aspinall et al.~\cite{Aspinall2010}. \paragraph{Verified compilation}
Note: See TracChangeset for help on using the changeset viewer.