14 Pages
English

A META LANGUAGE FOR TYPE CHECKING AND INFERENCE

-

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
A META LANGUAGE FOR TYPE CHECKING AND INFERENCE An Extended Abstract Amy Felty and Dale Miller Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104–6389 USA Abstract We present a logic, L?, in which terms are the simply typed ?-terms and very restricted, second-order quantification of functional variables is allowed. This logic can be used to directly encode the basic type judgments of a wide variety of typed ?-calculi. Judgments such as “term M is of type A” and “M is a proof of formula A” are represented by atomic propositions in L? while inference rules and axioms for such type judgments become simple quantified formulas. Theorem proving in L? can be described simply since the necessary unification of ?-terms is decidable and if unifiers exist, most general unifiers exist. Standard logic programming techniques can turn the specification of inference rules and axioms in L? into implementations of type checkers and inferrers. Several different typed ?-calculi have been specified in L? and these specifications have been directly executed by a higher-order logic programming language. We illustrate such encoding into L? by presenting type checkers and inferrers for the simply typed ?-calculus and the calculus of constructions. This extended abstract will be presented at the 1989 Workshop on Programming Logic, B˚alstad, Sweden. Comments are welcome. Address correspondence to the authors at the address above or at “felty@linc.

  • either bound

  • terms into

  • typed ?-terms

  • free variable

  • simply typed

  • l? can

  • logic programming

  • order horn

  • being simply

  • higher-order hereditary


Subjects

Informations

Published by
Reads 8
Language English
AMETALANGUAGEFORTYPECHECKINGANDINFERENCEAnExtendedAbstractAmyFeltyandDaleMillerDepartmentUofniCveorsmitpyutoefrPaenndnsIynlfvoarnmiaationSciencePhiladelphia,PA191046389USAAbstractWepresentalogic,Lλ,inwhichtermsarethesimplytypedλ-termsandveryrestricted,second-orderquantificationoffunctionalvariablesisallowed.Thislogiccanbeusedtodirectlyencodethebasictypejudgmentsofawidevarietyoftypedλ-calculi.Judgmentssuchas“termMisoftypeA”and“MisaproofofformulaA”arerepresentedbyatomicpropositionsinLλwhileinferencerulesandaxiomsforsuchtypejudgmentsbecomesimplequantifiedformulas.TheoremprovinginLλcanbedescribedsimplysincethenecessaryunificationofλ-termsisdecidableandifunifiersexist,mostgeneralunifiersexist.StandardlogicprogrammingtechniquescanturnthespecificationofinferencerulesandaxiomsinLλintoimplementationsoftypecheckersandinferrers.Severaldifferenttypedλ-calculihavebeenspecifiedinLλandthesespecificationshavebeendirectlyexecutedbyahigher-orderlogicprogramminglanguage.WeillustratesuchencodingintoLλbypresentingtypecheckersandinferrersforthesimplytypedλ-calculusandthecalculusofconstructions.Thisextendedabstractwillbepresentedatthe1989WorkshoponProgrammingLogic,Ba˚lstad,Sweden.Commentsarewelcome.Addresscorrespondencetotheauthorsattheaddressaboveorat“felty@linc.cis.upenn.edu”or“dale@linc.cis.upenn.edu.”