source: Papers/polymorphic-variants-2012/polymorphic-variants.tex @ 2408

Last change on this file since 2408 was 2408, checked in by sacerdot, 7 years ago

...

File size: 2.7 KB
Line 
1\documentclass[smallextended]{svjour3}
2
3\smartqed
4
5\usepackage[english]{babel}
6\usepackage[colorlinks]{hyperref}
7\usepackage{microtype}
8
9
10\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
11\title{Polymorphic variants in dependent type theory\thanks{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881.}}
12
13\institute{
14  Dominic P. Mulligan \at
15  Computer Laboratory,\\
16  University of Cambridge.
17  \email{dominic.p.mulligan@gmail.com} \and
18  Claudio Sacerdoti Coen \at
19  Dipartimento di Scienze dell'Informazione,\\
20  Universit\`a di Bologna.
21  \email{sacerdot@cs.unibo.it}
22}
23
24\begin{document}
25
26\maketitle
27
28\begin{abstract}
29
30Big long abstract introducing the work
31
32\keywords{Polymorphic variants \and dependent type theory \and Matita theorem prover}
33
34\end{abstract}
35
36%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
37% Section
38%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
39\section{Introduction}
40\label{sect.introduction}
41
42\section{Polymorphic variants}
43\begin{itemize}
44 \item General introduction, motivations
45 \item Bounded vs not-bounded.
46\end{itemize}
47
48\subsection{Subtyping as instantiation vs subtyping as safe static cast}
49
50\subsection{Syntax \& type checking rules}
51The ones of Guarrigue + casts, but also for the bounded case?
52Casts support both styles of subtyping.
53
54\subsection{Examples}
55The weird function types that only work in subtyping as instantiation
56
57\subsection{Solution to the expression problem}
58Our running example in pseudo-OCaml syntax
59
60\section{Bounded polymorphic variants via dependent types}
61Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
62\subsection{Simulation (reduction + type checking)}
63\subsection{Examples}
64The weird function types redone
65\subsection{Subtyping as instantiation vs subtyping as safe static cast}
66Here we show/discuss how our approach supports both styles at once.
67\subsection{Solution to the expression problem, I}
68Using subtyping as cast, the file I have produced
69\subsection{Solution to the expression problem, II}
70Using subtyping as instantiation, comparisons, pros vs cons
71\subsection{Negative encoding (??)}
72The negative encoding and application to the expression problem
73\subsection{Other encodings (??)}
74Hints to other possible encodings
75
76\section{Extensible records (??)}
77
78\section{Comparison to related work and alternatives}
79\begin{itemize}
80 \item Disjoint unions: drawbacks
81 \item Encoding the unbounded case: drawbacks
82\end{itemize}
83
84\section{Appendix: interface of library functions used to implement everything}
85
86\end{document}
Note: See TracBrowser for help on using the repository browser.