[Prev][Next][Index][Thread]
CADE-13 Workshop on Proof search in Type-Theoretic Languages
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
[ Apologies to those who receive this many times through different channels ]
Dear colleague,
Please find enclosed the first 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).
Best regards
Didier Galmiche
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
FIRST CALL FOR CONTRIBUTIONS
CADE-13 Workshop on
PROOF SEARCH IN TYPE-THEORETIC LANGUAGES
Rutgers University (New Brunswick, USA)
Tuesday 30th July, 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 12, 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
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 12, 1996
Notification of acceptance: June 1, 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 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
}
\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 12, 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 12, 1996}
\info {Notification of acceptance:} {June 1, 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
\\ 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}