A META LANGUAGE FOR TYPE CHECKING AND INFERENCE
14 pages
English

A META LANGUAGE FOR TYPE CHECKING AND INFERENCE

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
14 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

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


Sujets

Informations

Publié par
Nombre de lectures 13
Langue English

Exrait

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.”
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents