Skip to content

Commit

Permalink
Minor wording fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
0xd34df00d committed Jan 1, 2021
1 parent 33fcae8 commit ea39f5b
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions tex/paper.mng
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ Moreover, we do not consider the peculiarities of a specific algorithm performin
introducing instead the abstraction of a \emph{subtyping oracle}.
This allows plugging in not just SMT solvers but arbitrary decision procedures as long as they have certain properties we describe later.

This translation to a core dependently typed language provides several nice metatheoretical properties:
This translation to a core dependently typed language provides several nice metatheoretical properties, most importantly:
\begin{itemize}
\item Dependent types are a well-studied and well-understood subject,
so taking them as the translation target automatically provides us with the existing array of metatheorems.
Expand Down Expand Up @@ -160,7 +160,7 @@ and no prior papers strived to mechanically verify the metatheoretical propertie

\section{Motivation}

Having refinement types and dependent types in a single language is useful in multiple ways.
Having refinement types and dependent types in a single language is useful for many reasons.

Firstly, refinement types indeed lower the cognitive load and the amount of (both keyboard and mathematical) typing the programmer has to do.
As an example, consider a function taking two non-negative numbers $x, y$ and returning $x + y + x$ along with a proof that each summand is less than or equal to the sum.
Expand Down

0 comments on commit ea39f5b

Please sign in to comment.