[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 %%%%%%%%%%%%%%%%%%%