ionchy
/
CIS6700-Spring2025
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add link to development

This commit is contained in:
Jonathan Chan 2025-04-21 14:48:13 -04:00
parent e0811ff06f
commit 6374d0a819
3 changed files with 6 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
cbpv.mng
View File

@ -68,7 +68,8 @@ and the mutual values and computations of CBPV,
combined with the even more complex mutual inductives from POPLMark Reloaded,
make it an attractive test case to test the tactic's robustness.
This report is divided in roughly the same shape as the proof development.
This report is divided in roughly the same shape as the proof development.%
\footnote{\url{https://github.com/ionathanch/MutualInduction/tree/main/CBPV}}
\Cref{sec:syntax} introduces the syntax and the typing rules for CBPV (\texttt{Syntax.lean}, \texttt{Typing.lean}).
Then the inductive characterization of strong normalization is defined in \cref{sec:sn-ind} (\texttt{NormalInd.lean}),
followed by the logical relation in \cref{sec:lr} (\texttt{OpenSemantics.lean}).

BIN
cbpv.pdf (Stored with Git LFS)
View File

Binary file not shown.

3
cbpv.tex
View File

@ -68,7 +68,8 @@ and the mutual values and computations of CBPV,
combined with the even more complex mutual inductives from POPLMark Reloaded,
make it an attractive test case to test the tactic's robustness.
This report is divided in roughly the same shape as the proof development.
This report is divided in roughly the same shape as the proof development.%
\footnote{\url{https://github.com/ionathanch/MutualInduction/tree/main/CBPV}}
\Cref{sec:syntax} introduces the syntax and the typing rules for CBPV (\texttt{Syntax.lean}, \texttt{Typing.lean}).
Then the inductive characterization of strong normalization is defined in \cref{sec:sn-ind} (\texttt{NormalInd.lean}),
followed by the logical relation in \cref{sec:lr} (\texttt{OpenSemantics.lean}).