I would move the abstract to a new page
Dedication
- change "bachelor" to "bachelor's degree"
2 Background
- I would consider maybe italicizing your code words in the paragraphs. It is hard to tell the difference in some cases when viewing your paper on the computer. For example the code word "a" or "insert"
- Maybe don't use insert as a non code word because it can be confusing when you are referring to the function and when you are referring to the verb especially when both are used in the same sentence.
- "For insert, the length of the list is incremented by 1 every time one inserts a new element. " Is the first insert a code word or regular word? If it is a code word, it is not bolded.
- "the first(i.e. smallest) element " Do you need a space after the word 'first'? I think it might look better if you do.
- "Consider the tail of the list, i.e. xs. " Remove the i.e. in this sentence because you are stating the name of the tail of the list not giving an example of a tail.
2.4.4
- "Dependent Haskell introduce what’s known as a type family. " change "introduce "to "introduces"
- "Type family is a function defined at type level that returns a type. " This sentence is confusing due to 'type' being used multiple times very close together. Maybe use a synonym if possible or give an example of what you mean.
- "the resulting list is expected to have length the sum of the lengths of the two original lists " Confusing sentence. Maybe try to remove the first use of 'length'
- "First we want to show that concatenating an empty list with any other list l2 results in a list of length the sum of zero and the length of l2." Your l2 looks like the number 12. I would choose a different letter or add more letter to the name. I took me a long time to realize it wasn't the number. Also add a comma after 'First''
- "Also it worth mentioning " missing the word 'is'. Should change to "Also, it is worth mentioning" or "It is also worth mentioning"
- "As an effectful language, F* categorizes programming effects and in addition divergence in its type system. " Not sure what this sentence is saying
- "Second, one applies the type parameter (a:Type) before colon instead of as the first type parameter after the colon. " add the word 'the' before the first use of 'colon'
- "The reason to declare (a:Type) before colon is to bring " Do the same here.
2.5.3
- "F* in general supports two approach for verifying programs " Make 'approach' to 'approaches'
- "These two ways towards verification are often called the intrinsic and extrinsic style." "These two ways towards verification" this part sounds weird/confusing.
2.5.5
- l's look like 1's. It can be a bit confusing
- "If, instead, one can’t find any termination " Never use contractions in formal paper writing. Change 'can't' to 'cannot'
This section might be going into too much detail.
3 Approach and Novelty
- "These two approaches towards potentially non-terminating functions is measured by the strength and completeness of the type systems. " Change 'is' to 'are' in this sentence
4. Current Results
4.1.1.3
- I don't think you need to summarize. I think you can continue on
4.1.2
- "However, as a completely redesigned language that is relatively new, F* does not have many resources by now. " I would remove 'by now' or change to 'at this time.'
4.1.3
- "in GHC 8.0 doesn’t support any proof " Change 'doesn't' to 'does not'
- "It is a simple sorting algorithm that builds" I would change 'It' to 'Insertion sort'. Had to reread to figure out what 'it' was
- "It is equivalently to say that the output" Change 'equivalently' to 'equivalent' or change word all together. I would change the word. I don't think it is the right one to use in this case.
4.1.3.1
- "and separately prove on each of the three terms" Change 'prove on' to 'proves'?
- "syntax that worth mentioning " Add the word 'is' before 'worth'
- I am all for charts! It might help readers visualize and understand.
4.1.3.2
- "There are a lot of new syntax introduced here, so let’s discuss one by one " We word this tho make it more formal. The speech pattern/writing style changes here. Don't get too casual when everything else is formal. I would also start a new paragraph here.
- "a helper function that prove the first sorted lemma " Change 'prove' to 'proves'
- "The forall k. quantifier is the universal quantifier. " Spacing is off after 'k.' in paper
- I would add a new line after statement 4 to make it easier on the eyes
- "The last two part of our discussion is not expected " Change 'part' to 'parts' and 'is' to 'are'
- "Next we define the function insertion_sort in F*, as what we’ve " I would add a new line before here too to make it better on the eyes
Your tone seems to have change in this section. On page 32 especially. It gets pretty casual and on the next page's summary, it is more formal again. Try to keep it all the same tone and style
4.1.1.3
- "theorems, however, we start to find that F*’s interface get hard to use very " Remove 'however', it does not work here. Also, change 'get hard' it is too informal
4.2
- "Truly divergent functions don’t have many interesting properties that worth verify, so are not of our major concern. " Change 'don't' to 'do not' and 'verify' to 'verifying'. Add 'they' before 'are not' and change 'of our' to 'a'
- "verification-oriented language can’t verify properties on" Change 'can't' to 'cannot'
- Can tell you are starting to get tired at this point
4.2.1
- Change "doesn't"
- "Notice that our Consider the example calculating the quotient of 3 and " Remove "Notice that our"
- Change "doesn't"
4.2.2
4.2.2.2
- "Hence we provide the termination metric as " Add a comma after 'Hence'
- "Then we return back to the divergent division definition and move on to discuss a Peano division proof that is successfully verified. " Do you need the word 'Then' here? I find it a bit odd because we are starting a new section
- "In fact, the workaround we come up with, with some help " Change 'come' to 'came'
- Images! Always Images! I think it will be helpful
Very thorough paper but very tough to get through. I am not sure that you can help that though.