Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!cbatt!cbosgd!ucbvax!XX.LCS.MIT.EDU!LISA
From: LISA@XX.LCS.MIT.EDU (Lisa F. Melcher)
Newsgroups: mod.ai
Subject: Seminar - General Logic (MIT)
Message-ID: <12242024192.32.LISA@XX.LCS.MIT.EDU>
Date: Fri, 26-Sep-86 10:47:21 EDT
Article-I.D.: XX.12242024192.32.LISA
Posted: Fri Sep 26 10:47:21 1986
Date-Received: Tue, 30-Sep-86 20:14:50 EDT
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The ARPA Internet
Lines: 32
Approved: ailist@sri-stripe.arpa



                       Date: Thursday, October 2, 1986
                      Time: 1:45 p.m......Refreshments
                         Time: 2:00 p.m......Lecture
                             Place:  NE43 - 512A


                              " GENERAL LOGIC "

                               Gordon Plotkin
                       Department of Computer Science
                      University of Edinburgh, Scotland

                           
     A good many logics have been proposed for use in Computer Science.
Implementing them involves repeating a great deal of work.  We propose a
general account of logics as regards both their syntax and inference rules.
As immediate target we envision a system to which one inputs a logic
obtaining a simple proof-checker.  The ideas build on work in logic of
Paulson, Martin-Lof and Schroeder-Heister and in the typed lambda-calculus of
Huet and Coquand and Meyer and Reinhold.  The slogan is: Judgements are
Types.  For example the judgement that a proposition is true is identified
with its type of proofs; general and hypothetical judgements are identified
with dependent product types.  This gives one account of Natural Deduction.
It would be interesting to extend the work to consider (two-sided) sequent
calculi for classical and modal logics.


              Sponsored by TOC, Laboratory for Computer Science
                             Albert Meyer, Host
-------