## [7860bc]: thys / Locally-Nameless-Sigma / document / root.tex  Maximize  Restore  History

### 104 lines (78 with data), 3.0 kB

 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed %\usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage[greek,english]{babel} %option greek for \ %option english (default language) for \, \ %\usepackage[latin1]{inputenc} %for \, \, \, \, %\, \, \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Locally Nameless Sigma Calculus} \author{Ludovic Henrio and Florian Kamm\"uller and Bianca Lutz and Henry Sudhof} \maketitle \begin{abstract} We present a Theory of Objects based on the original functional $\varsigma$-calculus by Abadi and Cardelli \cite{AC96a} but with an additional parameter to methods. We prove confluence of the operational semantics following the outline of Nipkow's proof of confluence for the $\lambda$-calculus reusing his general \texttt{Commutation.thy} \cite{nip:01} a generic diamond lemma reduction. We furthermore formalize a simple type system for our $\varsigma$-calculus including a proof of type safety. The entire development uses the concept of Locally Nameless representation for binders \cite{ACPPW:POPL08}. We reuse an earlier proof of confluence \cite{HK:FMOODS07} for a simpler $\varsigma$-calculus based on de Bruijn indices and lists to represent objects. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography %\bibliographystyle{abbrv} %\bibliography{root} \bibliographystyle{entcs} \begin{thebibliography}{10} \bibitem{AC96a} M. Abadi and L. Cardelli. \newblock {A Theory of Objects''}. \newblock Springer, New York, 1996. \bibitem{ACPPW:POPL08} B. Aydemir, A, Chargu��raud, B.~C. Pierce, R. Pollack, and S. Weirich. \newblock Engineering formal metatheory. \newblock {\em Princ. of Programming Languages, POPL'08}, ACM, 2008. \bibitem{HK:FMOODS07} L. Henrio and F. Kamm��ller. \newblock A mechanized model of the theory of objects. \newblock {\em Formal Methods for Open Object-Based Distributed Systems,}. LNCS \textbf{4468} Springer, 2007. \bibitem{nip:01} Tobias Nipkow. \newblock{More Church Rosser Proofs.} \newblock{\em Journal of Automated Reasoning}. \newblock{\textbf{26}:51--66, 2001.} \end{thebibliography} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: