Commit 0951da00 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Update of the submission

parent 37fd1819
......@@ -77,11 +77,10 @@
\SCT{} \cite{sizechangetool} is a fully automated termination checker for the $\lm\Pi$-calculus modulo rewriting.
Its development was essential, when various libraries were encoded in an implementation of this logic:
\Dedukti{} \cite{dowekAl19Dk}.
the logical framework \Dedukti{} \cite{dowekAl19Dk}.
It is a logical framework,
meaning that the user can define the logic he wants to reason with and then use it to actually write proofs.
To define a logic, the user provides a set of rewriting rules.
A logical framework allows the user to define the logic he wants to reason with and then use it to actually write proofs.
In \Dedukti{}, to define a logic the user provides a set of rewriting rules.
Those rules do not only define functions, but can also define types.
However, to ensure that the defined type system has good properties, like logical consistency or decidability, the rules must satisfy some properties:
termination, confluence and type preservation.
......@@ -95,6 +94,8 @@ However, one can deplore the small number of participants in this category: Only
This lack of implementations is even more visible for rewriting with dependent types, for which criteria have been developed \cite{blanqui05mscs,jouannaud15tlca},
but as far as the author knows, none of them have been implemented.
\vspace{.3em}
\noindent{\bf Outline}
After presenting the logical system and examples of programs in \indsec{sect-lmp}, we present the criterion used by the tool in \indsec{sect-dp-sct}.
\indsec{sect-implem} details the implementation choices of \SCT{} and \indsec{sect-others} compares it with the others termination checkers.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment