# {Title of Paper}

<!-- the bold and italic text are meant to be fixed -->
<!-- the regular text blocks are meant to serve as examples, to help get started -->

## 1. New words and notions

_A list of words / notions you had to look up, along their definition if possible._

1. merge conflict - when git is unable to automatically resolve difference
2. cherry pick - choosing arbitrary commit by reference and append to HEAD
3. ...

## 2. Summarized abstract

_A very brief reformulation of the paper's abstract._

Paper discusses development and formal verification of CompCert. Verified 
compiler is useful for critical software as it guarantees safety properties 
of source code hold for the executable compiled code as well.

## 3. Interesting references

_A list of references you would like to consult._

<!-- Would you judge by title alone what looks interesting, or look up abstract and then decide? 
    Does this need more context on why something seems interesting?  --> 

1. Leroy, X. Formal certification of a compiler back-end, or: programming a 
    compiler with a proof assistant.
2. ...

## 4. Foundational gaps

_Specify any gaps you had in reading the paper._

- Section 3.5 "inductive types" assumes prior understanding of
    Calculus of Inductive Construction, and without the examples are unclear.

## 5. Quality of paper

_A general comment on the quality of the paper._

- is the writing coherent and easy to follow, clear of typos, etc.
- what does the paper introduce or how does it extend state of the art?
- any other quality attributes...

## 6. Publication

_Where was the paper published and what kind of venue is it._

It was published at LICS 2020 conference. The LICS Symposium is an annual 
international forum on theoretical and practical topics in computer science 
that relate to logic, broadly construed.
    
## 7. Cited by
    
_Perform Google Scholar reverse search to find examples of who cites this paper and in what context._

1. Ben-Amram, A: "Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time":
    Builds on mwp analysis by adding more expressive complexity certificates.
    
2. Hainry, E: "Type-based complexity analysis for fork processes":
    mwp analysis is mentioned as "related works", for theoretical complexity
    analysis based on matrix calculus.    
    
3. ...                  

## 8. Bib entry

<!-- add ref -->

## 9. Open questions

_These questions may be formulated by the authors themselves or by yourself._

- if mwp analysis could be applied to richer languages 
- how powerful the analysis methods are
- how to handle more elaborate examples, e.g. recursive functions
- (other questions specific to paper)