[Prev][Next][Index][Thread]
CFP: Proof search in type-theoretic languages
Dear Colleague,
Please find enclosed the call announcement for participation to the
CADE-12 Workshop "Proof search in type-theoretic languages" which
will be held during one full day (June 26, 1994) in conjunction with
CADE-12 Conference.
Information requests should be sent to the workshop organizers:
D. Galmiche, Nancy, e-mail: Didier.Galmiche@loria.fr
L. Wallen, Oxford, e-mail: Lincoln.Wallen@prg.ox.ac.uk
Didier Galmiche.
----------------------------------------------------------------------
Call for Workshop Participation (CADE-12)
PROOF SEARCH IN TYPE-THEORETIC LANGUAGES
Nancy, France, June 26, 1994
This workshop will focus on the problems of proof search in
type-theoretic languages. Such languages are used as logical
frameworks for representing proofs and, in some cases, formalize
connections between proofs and programs that support program
synthesis.
The purpose of the workshop is to discuss recent results
in, and to establish and publicize a research agenda for, proof search
in type theories and their use in the formal development of correct
proofs and programs.
Topics:
------
The workshop is intended to bring together researchers interested in
all aspects of proof search in type-theoretic languages, including but
not limited to the following topics:
* foundations of proof search in type theory frameworks
* techniques and concepts related to proof construction
and related analysis
* proof synthesis vs program synthesis (applications, specific methods)
* environments for formal proof development in type-theoretic frameworks
Workshop:
--------
The workshop is held, during one full day (June 26, 1994),
in conjunction with CADE-12 Conference). Attendance is by invitation
only: authors of accepted submissions will be invited. Informal
proceedings will be supplied by the CADE organizing committee.
Submission:
----------
Researchers interested in presenting their work are invited to send an
extended abstract (5-7 pages) to each of the organizers named below.
Researchers interested in attending the workshop (without giving a
presentation) should send a position paper (1-2 pages) presenting
their interest.
e-mail submissions (*.dvi or *.ps files) are requested
(hardcopies are also accepted) before April 8, 1994. Notification of
acceptance and invitations to the workshop will be issued by
May 5, 1994. Material to be handed out at the workshop should be
received in final form before May 24, 1994.
All submissions and information requests should be sent to the
workshop organizers:
Didier Galmiche Lincoln Wallen
CRIN-CNRS & INRIA Lorraine Computing Laboratory
Campus Scientifique, B.P. 239 University of Oxford
54506 Vandoeuvre-les-Nancy, Parks Road, Oxford OX1 3QD,
France U.K.
email: Didier.Galmiche@loria.fr email: Lincoln.Wallen@prg.ox.ac.uk
fax: [+33] 83 41 30 79 fax: [+44] 865 27 38 39
Deadlines
---------
Deadline for submission: April 8, 1994
Notification of acceptance: May 5, 1994
Abstract final version: May 24, 1994
Program Committee:
------------------
D. Galmiche (CRIN-CNRS & INRIA, Nancy)
L. Helmink (Philips Research Laboratories, Eindhoven)
F. Pfenning (Carnegie Mellon University, Pittsburgh)
S. Thompson (University of Kent)
L. Wallen (University of Oxford)
%%%%%%%%%%%%%%%%%%%%%% LaTeX Version %%%%%%%%%%%%%%%%%%%
\documentstyle[11pt]{article}
\setlength{\oddsidemargin}{0cm}
\setlength{\evensidemargin}{0cm}
\setlength{\textwidth}{16cm}
\setlength{\topmargin}{0cm}
\setlength{\headsep}{0.0in}
\setlength{\textheight}{25cm}
\pagestyle{empty}
\setlength{\parindent}{0cm}
\begin{document}
\begin{center}
{\large \bf Call for Workshop Participation (CADE-12)}\\
~\\
~\\
{\LARGE \bf Proof search in type-theoretic languages}\\
~\\
~\\
{\large \bf Nancy, France, June 26, 1994}
\end{center}
~\\
~\\
This workshop will focus on the problems of proof search in
type-theoretic languages. Such languages are used as logical
frameworks for representing proofs and, in some cases, formalize
connections between proofs and programs that support program
synthesis. \\
The purpose of the workshop is to discuss recent results
in, and to establish and publicize a research agenda for, proof search
in type theories and their use in the formal development of correct
proofs and programs.\\
~\\
{\bf Topics:} The workshop is intended to bring together researchers
interested in all aspects of proof search in type-theoretic languages,
including, but not limited to, the following topics:\\
~\\
\hspace*{10mm} $\bullet$ foundations of proof search in type theory
frameworks \\
\hspace*{10mm} $\bullet$ techniques and concepts related to proof
construction and related analysis \\
\hspace*{10mm} $\bullet$ proof synthesis vs program synthesis
(applications, specific methods) \\
\hspace*{10mm} $\bullet$ environments for formal proof development in
type-theoretic frameworks \\
~\\
{\bf Workshop:} The workshop is held, during one full-day (June 26, 1994),
in conjunction with CADE-12 Conference). Attendance is by invitation
only: authors of accepted submissions will be invited. Informal
proceedings will be supplied by the CADE organizing committee. \\
~\\
{\bf Submission:}
Researchers interested in presenting their work are invited to send an
{\bf extended abstract (5-7 pages)} to each of the organizers named below.
Researchers interested in attending the workshop (without giving a
presentation) should send a position paper (1-2 pages) presenting
their interest. {\bf e-mail submissions} ($\star$.dvi or $\star$.ps
files) are requested (hardcopies are also accepted) before {\bf
April 8, 1994}. Notification of acceptance and invitations to the
workshop will be issued by {\bf May 5, 1994}. Material to be handed
out at the workshop should be received in final form before {\bf May 24,
1994}. \\
~\\
All submissions and information requests should be sent to the {\bf workshop organizers}:
\begin{center}
\begin{tabular}{l}
Didier Galmiche \\
CRIN-CNRS $\&$ INRIA Lorraine \\
Campus Scientifique, B.P. 239 \\
54506 Vand\oe uvre-l\`es-Nancy,
France \\
email: Didier.Galmiche@loria.fr \\
fax: [+33] 83 41 30 79 \\
\end{tabular}
\hspace*{2cm}
\begin{tabular}{l}
Lincoln Wallen \\
Computing Laboratory \\
University of Oxford \\
Parks Road, Oxford OX1 3QD,
U.K. \\
email: Lincoln.Wallen@prg.ox.ac.uk \\
fax: [+44] 865 27 38 39
\end{tabular}
\end{center}
\begin{tabular}{l}
{\bf Program Committee:}\\
D. Galmiche (CRIN-CNRS $\&$ INRIA, Nancy) \\
L. Helmink (Philips Research Laboratories, Eindhoven)\\
F. Pfenning (Carnegie Mellon University, Pittsburgh) \\
S. Thompson (University of Kent) \\
L. Wallen (University of Oxford) \\
\end{tabular}
\hspace*{3mm}
\begin{tabular}{l}
{\bf Important dates}:\\
Submission due: \hspace*{17mm} April \hspace*{0.3mm} 8, 1994 \\
Notification of Acceptance: May \hspace*{1mm} 5, 1994 \\
Abstract final version: \hspace*{7mm} May 24, 1994 \\
\end{tabular}
\end{document}
%%%%%%%%%%%%%%%%%%%%%% END LaTeX Version %%%%%%%%%%%%%%%%%%%