Different Schools

Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

Mail folder: QED
Next message: jt@linus.mitre.org: "illusion"
Previous message: David McAllester: "Different Schools"
Maybe in reply to: David McAllester: "Different Schools"

To: qed@mcs.anl.gov
Subject: Different Schools
Date: Tue, 20 Apr 93 16:29:09 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-id: <"swan.cl.cam.:080740:930420152927"@cl.cam.ac.uk>
Sender: qed-owner
Precedence: bulk


Translation (or interpretation) between different schools is one of the key
issues.  We also need translation to import theories from other systems.

A common "lingua franca" could be valuable; it is another of the key issues. 
Should this merely formalize assertions, or should it also capture aspects of
their proofs, like the "mathematical vernacular" (de Bruijn's concept)?

Making the "lingua franca" neutral will not be easy.  The if-then-else
construct, descriptions and powersets are unacceptable in certain schools.  I
also fear disagreement on whether the "lingua franca" should be typed or
untyped (I prefer the latter).

							Larry Paulson