equal
deleted
inserted
replaced
1 \documentclass[10pt, conference, compsocconf]{IEEEtran} |
1 \documentclass[runningheads]{llncs} |
|
2 %\documentclass[10pt, conference, compsocconf]{IEEEtran} |
2 \usepackage{isabelle} |
3 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
4 \usepackage{isabellesym} |
4 \usepackage{times} |
5 \usepackage{times} |
5 \usepackage{amssymb} |
6 \usepackage{amssymb} |
6 \usepackage{amsmath} |
7 \usepackage{amsmath} |
23 \renewcommand{\isasymiota}{} |
24 \renewcommand{\isasymiota}{} |
24 \newcommand{\isasymulcorner}{$\ulcorner$} |
25 \newcommand{\isasymulcorner}{$\ulcorner$} |
25 \newcommand{\isasymurcorner}{$\urcorner$} |
26 \newcommand{\isasymurcorner}{$\urcorner$} |
26 \begin{document} |
27 \begin{document} |
27 |
28 |
|
29 |
28 \title{Formalising Computability Theory in Isabelle/HOL} |
30 \title{Formalising Computability Theory in Isabelle/HOL} |
29 |
31 \author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}} |
30 |
32 \institute{PLA University of Science and Technology, China \and King's College London, UK} |
31 \author{ |
|
32 \IEEEauthorblockN{Jian Xu, Xingyuan Zhang} |
|
33 \IEEEauthorblockA{PLA University of Science and Technology Nanjing, China} |
|
34 \and |
|
35 \IEEEauthorblockN{Christian Urban} |
|
36 \IEEEauthorblockA{King's College London, UK} |
|
37 } |
|
38 |
33 |
39 \maketitle |
34 \maketitle |
40 |
35 |
41 |
36 |
42 \begin{abstract} |
37 \begin{abstract} |
50 functions. Our theory can be used to formalise other computability results: |
45 functions. Our theory can be used to formalise other computability results: |
51 we give one example about the undecidability of Wang's tiling problem, whose proof uses |
46 we give one example about the undecidability of Wang's tiling problem, whose proof uses |
52 the notion of a universal Turing machine. |
47 the notion of a universal Turing machine. |
53 \end{abstract} |
48 \end{abstract} |
54 |
49 |
55 \begin{IEEEkeywords} |
|
56 Turing Machines, Computability, Isabelle/HOL, Wang tilings |
|
57 \end{IEEEkeywords} |
|
58 |
|
59 |
|
60 \IEEEpeerreviewmaketitle |
|
61 |
|
62 % generated text of all theories |
50 % generated text of all theories |
63 \input{session} |
51 \input{session} |
64 |
52 |
65 % optional bibliography |
53 % optional bibliography |
66 \bibliographystyle{abbrv} |
54 \bibliographystyle{abbrv} |