[Prev][Next][Index][Thread]
types
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
[ Note the change of deadline from 12 May to 19 May.
-- Philip Wadler, moderator, Types Forum.]
[ Apologies to those who receive this many times through different
channels ]
Dear colleague,
Please find enclosed the last Call for Contributions (ascii and latex
files) for the CADE-13 Workshop on "Proof search in Type-Theoretic
Languages", Tuesday 30th July, 1996, Rutgers University (New
Brunswick, USA).
Extended dealine: May 19, 1996.
Best regards
Didier Galmiche
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
LAST CALL FOR CONTRIBUTIONS
CADE-13 Workshop on
PROOF SEARCH IN TYPE-THEORETIC LANGUAGES
Rutgers University (New Brunswick, USA)
Tuesday 30th July, 1996
EXTENDED DEADLINE: May 19, 1996
-----------------
A one day workshop on "Proof Search in Type-Theoretic Languages"
will be held the 30th July 1996 in conjunction with the 13th Conference
in Automated DEduction (CADE-13, Rutgers University, New Brunswick,
USA). Attendance is by invitation only: authors of accepted
submissions will be invited. Informal proceedings will be supplied by
the CADE-13 organizing committee.
TOPICS
Many recent works have been devoted to type theory and its
applications to proof and program development in various logical
frameworks. This workshop focuses on proof search in type-theoretic
languages and their underlying logics. Such languages are logical
frameworks for representing proofs and in some cases formalize
connections between proofs and programs that support program
synthesis.
The workshop is intended to bring together researchers interested in all
aspects of proof search in type-theoretic languages.
The objective is to provide an integrated forum for the presentation
of research and the exchange of ideas and experiences in the topics
concerned with proof search in type theory, logical frameworks and
their underlying (classical, intuitionistic and linear) logics.
Topics of interest, in this context, include (but are not restricted
to):
- foundations of proof search,
- techniques and concepts related to proof construction,
- logic programming,
- proof synthesis vs program synthesis,
- applications,
- equational theories and rewriting,
- decision procedures,
- environments for formal proof development.
SUBMISSIONS
Researchers interested in presenting their works are invited to send an
extended abstract (5-8 pages) by e-mail submissions of
Postscript files to the Organizing-Program Chair
(Didier.Galmiche@loria.fr) before May 19, 1996.
Researchers interested in attending the workshop (without giving a
presentation) should send a position paper (1-2 pages) presenting
their interest.
Papers will be reviewed by peers, typically members of the program
committee. The cover page should include a return mailing address
and, if possible, an electronic mail address and a fax number.
Additional information will be available through WWW address:
http://www.loria.fr/~galmiche/cade96-wp6.html.
INFORMATION
Organizing-Program Chair
D. Galmiche
CRIN-CNRS, UHP Nancy I
Batiment LORIA
54506 Vandoeuvre-les-Nancy
France
Phone: +33 83 59 20 15
Fax: +33 83 41 30 79
email: Didier.Galmiche@loria.fr
URL: http://www.loria.fr/~galmiche/cade96-wp6.html
Organizing-Program Committee:
D. Galmiche (CRIN-CNRS, Nancy)
F. Pfenning (CMU, Pittsburgh)
N. Shankar (SRI, Stanford)
J. Smith (Chalmers University, G\"{o}teborg)
L. Wallen (Oxford University)
IMPORTANT DATES
Deadline for submissions: May 19, 1996
Notification of acceptance: June 5, 1996
Workshop handouts ready: June 22, 1996
Workshop date: July 30, 1996
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LATEX FILE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentstyle{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Call for papers %%
%% CADE-13 workshop WP-6 %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\head{
{\Large \bf LAST CALL FOR CONTRIBUTIONS
}\\[3mm]
{\large \bf CADE-13 Workshop on
}\\[4mm]
{\Large \bf Proof Search in Type-Theoretic Languages} \\
~\\
{\bf Rutgers University (New Brunswick, USA)}\\
Tuesday 30th July, 1996 \\
~\\
EXTENDED DEADLINE : May 19, 1996
}
\def\body{
\sect{
}
A one day workshop on {\em Proof Search in Type-Theoretic Languages}
will be held the 30th July 1996 in conjunction with the 13th Conference
in Automated DEduction (CADE-13, Rutgers University, New Brunswick,
USA). Attendance is by invitation only: authors of accepted
submissions will be invited. Informal proceedings will be supplied by
the CADE-13 organizing committee.
\sect{ TOPICS
}
Many recent works have been devoted to type theory and its
applications to proof and program development in various logical
frameworks. This workshop focuses on proof search in type-theoretic
languages and their underlying logics. Such languages are logical
frameworks for representing proofs and in some cases formalize
connections between proofs and programs that support program
synthesis.\\
~\\
The workshop is intended to bring together researchers interested in all
aspects of proof search in type-theoretic languages.
The objective is to provide an integrated forum for the presentation
of research and the exchange of ideas and experiences in the topics
concerned with proof search in type theory, logical frameworks and
their underlying (classical, intuitionistic and linear) logics.\\
~\\
Topics of interest, in this context, include (but are not restricted
to):
\items{
\item foundations of proof search
\item techniques and concepts related to proof construction
\item logic programming
\item proof synthesis vs program synthesis
\item applications
\item equational theories and rewriting
\item decision procedures
\item environments for formal proof development.
}
\sect{ SUBMISSIONS
}
Researchers interested in presenting their works are invited to send an
{\bf extended abstract (5-8 pages)} by {\bf e-mail submissions} of
Postscript files to the Organizing-Program Chair ({\bf
Didier.Galmiche@loria.fr}) before {\bf May 19, 1996}.
Researchers interested in attending the workshop (without giving a
presentation) should send a position paper (1-2 pages) presenting
their interest.
Papers will be reviewed by peers, typically members of the program committee.
The cover page should include a return mailing address and, if
possible, an electronic mail address and a fax number.
Additional information will be available through WWW address: {\bf
http://www.loria.fr/$^\sim$galmiche/cade96-wp6.html}.
}
% PRACTICAL INFORMATION
\def\pract{
\inform{ CADE-13 WP-6
}{
\names{ Organizing-Program Chair:
}
~\\
D. Galmiche (CRIN-CNRS, Nancy)
\\[3mm]
\names{ Organizing-Program Committee:
}
~\\
D. Galmiche (CRIN-CNRS, Nancy) \\
~\\
F. Pfenning (CMU, Pittsburgh) \\
~\\
N. Shankar (SRI, Stanford) \\
~\\
J. Smith (Chalmers Univ, G\"{o}teborg) \\
~\\
L. Wallen (Oxford University)
}
~\\
~\\
~\\
\inform{ IMPORTANT DATES
}{\cent{
\info {Deadline for submissions:} {May 19, 1996}
\info {Notification of acceptance:} {June 5, 1996}
\info {Workshop handouts ready:} {June 22, 1996}
\info {Workshop date:} {July 30, 1996}
}}
~\\
~\\
~\\
\inform{ INFORMATION
}{
\infow {by email:} {galmiche@loria.fr}
\infow {by URL:}
{http://www.loria.fr/$^\sim$galmiche/ \\ cade96-wp6.html}
\infow {by surface mail:} {D. Galmiche
\\ CADE-13 WP-6
\\ CRIN-CNRS, UHP Nancy I
\\ Batiment LORIA
\\ 54506 Vandoeuvre-les-Nancy
\\ France
\\ Phone: +33 83 59 20 15
\\ Fax: +33 83 41 30 79
}
}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The text below will format this announcement with LaTeX
% in a style designed by Jeroen Fokker, Utrecht University (jeroen@cs.ruu.nl),
% which has been adapted for our purposes
\pagestyle{empty}
\topmargin-10mm \oddsidemargin-20mm \textwidth190mm \textheight26cm
\newcommand{\cent}[1]{\begin{center}#1\end{center}}
\newcommand{\names}[1]{{\bf #1}\\[0.5mm]}
\newcommand{\info}[2]{{\em #1}\\ ~\\ {\bf #2}\\[2mm]}
\newcommand{\infow}[2]{{\em #1}\\ {\bf #2}\\[2mm]}
\newcommand{\sect}[1]{\vspace{7mm}\par\centerline{{\bf #1}}\vspace{4mm}\par}
\newcommand{\items}[1]{\vspace{3mm}\begin{itz} #1
\end{itz}\vspace{3mm}\par}
\newcommand{\inform}[2]{
\fbox{\begin{minipage}[t]{51mm}
\vspace{2mm}\par
\centerline{#1}\footnotesize\vspace{1mm}\par#2
\end{minipage}}\vspace{3mm}
}
\newenvironment{itz}{
\begin{list}{$\bullet$}{
\parsep=0pt\parskip=0pt\topsep=0pt\itemsep=0pt\leftmargin=1em
}}{\end{list}}
\begin{document}
\nopagebreak
\begin{minipage}[t]{55mm}
\vspace*{46mm}
\pract
\end{minipage}
\hfill
\begin{minipage}[t]{128mm}
{\large\sl\cent{\head}}
\body
\end{minipage}
\end{document}