Automatically assigned DDC number: 005131
Manually assigned DDC number: 005131
Number of references: 16
Title: Some Lambda Calculus and Type Theory Formalized
Author:
Author:
Subject: James Mckinna,Robert Pollack Some Lambda Calculus and Type Theory Formalized
Description: . We survey a substantial body of knowledge about lambda calculus and Pure Type Systems, formally developed in a constructive type theory using the LEGO proof system. On lambda calculus, we work up to an abstract, simplified, proof of standardization for beta reduction, that does not mention redex positions or residuals. Then we outline the meta theory of Pure Type Systems, leading to the strengthening lemma. One novelty is our use of named variables for the formalization. Along the way we point out what we feel has been learned about general issues of formalizing mathematics, emphasizing the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts. Keywords: formal mathematics, lambda calculus, Pure Type Systems, type theory, LEGO proof checker. 1. Introduction "This paper is about our hobby." That is the first sentence of [30], the first report on our formal development of lambda calculus and type theory, written ...
Contributor: The Pennsylvania State University CiteSeer Archives
Publisher: unknown
Date: 1999-06-18
Pubyear: 1998
Format: ps
Identifier: http://citeseer.ist.psu.edu/342020.html
Source: ftp://ftp.dcs.ed.ac.uk/pub/lego/McKinnaPollack97.ps.gz
Language: en
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Relation:
Rights: unrestricted
<?xml version="1.0" encoding="UTF-8"?>
<references_metadata>
<rec ID="/50693.html" Type="inproceedings" CiteSeer_Book="Proceedings of the International Conference on Typed Lambda Calculi and Applications" CiteSeer_Volume="" Title="A Formalization of the Strong Normalization Proof for {System F} in {LEGO},">
<identifier Org="ISBN:3540314288" Paper_ID="/50693.html" Extracted="3540314288" DDC="005.131" Normalized_DDC="005131" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540432876" Paper_ID="/50693.html" Extracted="3540432876" DDC="006.3/33" Normalized_DDC="006333" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540565175" Paper_ID="/50693.html" Extracted="3540565175" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540578269" Paper_ID="/50693.html" Extracted="3540578269" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540580859" Paper_ID="/50693.html" Extracted="3540580859" DDC="005.1/01/5113" Normalized_DDC="0051015113" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540605797" Paper_ID="/50693.html" Extracted="3540605797" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540664637" Paper_ID="/50693.html" Extracted="3540664637" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540665366" Paper_ID="/50693.html" Extracted="3540665366" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540679340" Paper_ID="/50693.html" Extracted="3540679340" DDC="346/.092" Normalized_DDC="346092" Normalized_Weight="0.1111111111111111" />
</rec>
<rec ID="/32039.html" Type="misc" CiteSeer_Book="" CiteSeer_Volume="" Title="Combinator Shared Reduction and Infinite Objects in Type Theory," />
<rec ID="/110243.html" Type="article" CiteSeer_Book="Science of Computer Programming" CiteSeer_Volume="26" Title="An Algorithm for Type-Checking Dependent Types,">
<identifier Org="ISBN:3540255931" Paper_ID="/110243.html" Extracted="3540255931" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:3540432876" Paper_ID="/110243.html" Extracted="3540432876" DDC="006.3/33" Normalized_DDC="006333" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:3540440445" Paper_ID="/110243.html" Extracted="3540440445" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:3540651373" Paper_ID="/110243.html" Extracted="3540651373" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:3540672575" Paper_ID="/110243.html" Extracted="3540672575" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:3540705937" Paper_ID="/110243.html" Extracted="3540705937" />
<identifier Org="ISBN:3540789685" Paper_ID="/110243.html" Extracted="3540789685" DDC="005.1/15" Normalized_DDC="005115" Normalized_Weight="0.16666666666666666" />
</rec>
<rec ID="/336682.html" Type="incollection" CiteSeer_Book="What is a Logical System" CiteSeer_Volume="" Title="Finitary Inductively Presented Logics,">
<identifier Org="ISBN:0198501277" Paper_ID="/336682.html" Extracted="0198501277" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:0198538596" Paper_ID="/336682.html" Extracted="0198538596" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:0198567936" Paper_ID="/336682.html" Extracted="0198567936" DDC="510.9" Normalized_DDC="5109" Normalized_Weight="0.0625" />
<identifier Org="ISBN:0387976671" Paper_ID="/336682.html" Extracted="0387976671" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:0415187095" Paper_ID="/336682.html" Extracted="0415187095" DDC="103" Normalized_DDC="103" Normalized_Weight="0.0625" />
<identifier Org="ISBN:0444874550" Paper_ID="/336682.html" Extracted="0444874550" />
<identifier Org="ISBN:052141413X" Paper_ID="/336682.html" Extracted="052141413X" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:0521433126" Paper_ID="/336682.html" Extracted="0521433126" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:1402006993" Paper_ID="/336682.html" Extracted="1402006993" DDC="160" Normalized_DDC="16" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540414134" Paper_ID="/336682.html" Extracted="3540414134" DDC="005" Normalized_DDC="005" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540433384" Paper_ID="/336682.html" Extracted="3540433384" DDC="006.3" Normalized_DDC="0063" Normalized_Weight="0.0625" />
<identifier Org="ISBN:354059132X" Paper_ID="/336682.html" Extracted="354059132X" DDC="005.7/3" Normalized_DDC="00573" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540605797" Paper_ID="/336682.html" Extracted="3540605797" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540637729" Paper_ID="/336682.html" Extracted="3540637729" DDC="004.2/1" Normalized_DDC="00421" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540651373" Paper_ID="/336682.html" Extracted="3540651373" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540781269" Paper_ID="/336682.html" Extracted="3540781269" DDC="004.0151" Normalized_DDC="0040151" Normalized_Weight="0.0625" />
<identifier Org="ISBN:8847007836" Paper_ID="/336682.html" Extracted="8847007836" DDC="121.65" Normalized_DDC="12165" Normalized_Weight="0.0625" />
</rec>
<rec ID="/3927.html" Type="phdthesis" CiteSeer_Book="" CiteSeer_Volume="" Title="Logics and Type Systems,">
<identifier Org="ISBN:1568812035" Paper_ID="/3927.html" Extracted="1568812035" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540005684" Paper_ID="/3927.html" Extracted="3540005684" DDC="510/.285" Normalized_DDC="510285" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540213139" Paper_ID="/3927.html" Extracted="3540213139" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540228497" Paper_ID="/3927.html" Extracted="3540228497" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540253882" Paper_ID="/3927.html" Extracted="3540253882" DDC="004" Normalized_DDC="004" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540282319" Paper_ID="/3927.html" Extracted="3540282319" DDC="005.1/015113" Normalized_DDC="0051015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:354030553X" Paper_ID="/3927.html" Extracted="354030553X" DDC="005.1/15" Normalized_DDC="005115" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540404384" Paper_ID="/3927.html" Extracted="3540404384" DDC="005.1/5" Normalized_DDC="00515" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540417397" Paper_ID="/3927.html" Extracted="3540417397" DDC="005.1/4" Normalized_DDC="00514" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540440445" Paper_ID="/3927.html" Extracted="3540440445" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540441441" Paper_ID="/3927.html" Extracted="3540441441" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540580859" Paper_ID="/3927.html" Extracted="3540580859" DDC="005.1/01/5113" Normalized_DDC="0051015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540605797" Paper_ID="/3927.html" Extracted="3540605797" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540630457" Paper_ID="/3927.html" Extracted="3540630457" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540657630" Paper_ID="/3927.html" Extracted="3540657630" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:354067778X" Paper_ID="/3927.html" Extracted="354067778X" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540799796" Paper_ID="/3927.html" Extracted="3540799796" />
<identifier Org="ISBN:3540921877" Paper_ID="/3927.html" Extracted="3540921877" />
</rec>
<rec ID="/466648.html" Type="inproceedings" CiteSeer_Book="Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL" CiteSeer_Volume="" Title="Five Axioms of Alpha-Conversion,">
<identifier Org="ISBN:0198501277" Paper_ID="/466648.html" Extracted="0198501277" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:1595930728" Paper_ID="/466648.html" Extracted="1595930728" DDC="005.13" Normalized_DDC="00513" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540201947" Paper_ID="/466648.html" Extracted="3540201947" DDC="005.1/1" Normalized_DDC="00511" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540230173" Paper_ID="/466648.html" Extracted="3540230173" DDC="511.36028563" Normalized_DDC="51136028563" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540280057" Paper_ID="/466648.html" Extracted="3540280057" DDC="006.3" Normalized_DDC="0063" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540405593" Paper_ID="/466648.html" Extracted="3540405593" DDC="006.3" Normalized_DDC="0063" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540406646" Paper_ID="/466648.html" Extracted="3540406646" DDC="006.3/33" Normalized_DDC="006333" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:354040709X" Paper_ID="/466648.html" Extracted="354040709X" />
<identifier Org="ISBN:3540418644" Paper_ID="/466648.html" Extracted="3540418644" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540421173" Paper_ID="/466648.html" Extracted="3540421173" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540429573" Paper_ID="/466648.html" Extracted="3540429573" DDC="005.11" Normalized_DDC="00511" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540440399" Paper_ID="/466648.html" Extracted="3540440399" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.08333333333333333" />
<identifier Org="ISBN:3540744630" Paper_ID="/466648.html" Extracted="3540744630" />
<identifier Org="ISBN:3540745904" Paper_ID="/466648.html" Extracted="3540745904" DDC="005.1/15" Normalized_DDC="005115" Normalized_Weight="0.08333333333333333" />
</rec>
<rec ID="/443676.html" Type="misc" CiteSeer_Book="" CiteSeer_Volume="" Title="Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs,">
<identifier Org="ISBN:1402006071" Paper_ID="/443676.html" Extracted="1402006071" DDC="004" Normalized_DDC="004" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:1402016565" Paper_ID="/443676.html" Extracted="1402016565" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:1586030159" Paper_ID="/443676.html" Extracted="1586030159" />
<identifier Org="ISBN:184150176X" Paper_ID="/443676.html" Extracted="184150176X" />
<identifier Org="ISBN:3540000291" Paper_ID="/443676.html" Extracted="3540000291" DDC="004/.01/51" Normalized_DDC="0040151" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540230173" Paper_ID="/443676.html" Extracted="3540230173" DDC="511.36028563" Normalized_DDC="51136028563" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540242872" Paper_ID="/443676.html" Extracted="3540242872" DDC="332.1/78" Normalized_DDC="332178" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540252363" Paper_ID="/443676.html" Extracted="3540252363" DDC="005.1/15" Normalized_DDC="005115" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540439285" Paper_ID="/443676.html" Extracted="3540439285" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540440399" Paper_ID="/443676.html" Extracted="3540440399" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540664637" Paper_ID="/443676.html" Extracted="3540664637" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540665374" Paper_ID="/443676.html" Extracted="3540665374" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540668365" Paper_ID="/443676.html" Extracted="3540668365" DDC="005" Normalized_DDC="005" Normalized_Weight="0.09090909090909091" />
<identifier Org="ISBN:3540921877" Paper_ID="/443676.html" Extracted="3540921877" />
</rec>
<rec ID="/348733.html" Type="incollection" CiteSeer_Book="TAPSOFT 91 Proceedings of the International Joint Conference on Theory and Practice of Software Development Brighton UK Volume 1 Colloquium on Trees in Algebra and Programming CAAP 91" CiteSeer_Volume="" Title="Program Specification and Data Refinement in Type Theory,">
<identifier Org="ISBN:0521433126" Paper_ID="/348733.html" Extracted="0521433126" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:0521580579" Paper_ID="/348733.html" Extracted="0521580579" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:0818676744" Paper_ID="/348733.html" Extracted="0818676744" DDC="005.3" Normalized_DDC="0053" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:0818676787" Paper_ID="/348733.html" Extracted="0818676787" DDC="005.16" Normalized_DDC="00516" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540215239" Paper_ID="/348733.html" Extracted="3540215239" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540404384" Paper_ID="/348733.html" Extracted="3540404384" DDC="005.1/5" Normalized_DDC="00515" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540539816" Paper_ID="/348733.html" Extracted="3540539816" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540565175" Paper_ID="/348733.html" Extracted="3540565175" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:354059132X" Paper_ID="/348733.html" Extracted="354059132X" DDC="005.7/3" Normalized_DDC="00573" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540605797" Paper_ID="/348733.html" Extracted="3540605797" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540605894" Paper_ID="/348733.html" Extracted="3540605894" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540616292" Paper_ID="/348733.html" Extracted="3540616292" DDC="005.7/3" Normalized_DDC="00573" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540627812" Paper_ID="/348733.html" Extracted="3540627812" DDC="005.1/2" Normalized_DDC="00512" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540631720" Paper_ID="/348733.html" Extracted="3540631720" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540633790" Paper_ID="/348733.html" Extracted="3540633790" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540651373" Paper_ID="/348733.html" Extracted="3540651373" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.058823529411764705" />
<identifier Org="ISBN:3540679340" Paper_ID="/348733.html" Extracted="3540679340" DDC="346/.092" Normalized_DDC="346092" Normalized_Weight="0.058823529411764705" />
</rec>
<rec ID="/279460.html" Type="inproceedings" CiteSeer_Book="TYPES" CiteSeer_Volume="" Title="Inverting Inductively Defined Relations in {LEGO},">
<identifier Org="ISBN:1581138504" Paper_ID="/279460.html" Extracted="1581138504" DDC="005.13/3" Normalized_DDC="005133" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540314288" Paper_ID="/279460.html" Extracted="3540314288" DDC="005.131" Normalized_DDC="005131" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540432876" Paper_ID="/279460.html" Extracted="3540432876" DDC="006.3/33" Normalized_DDC="006333" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540651373" Paper_ID="/279460.html" Extracted="3540651373" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540710655" Paper_ID="/279460.html" Extracted="3540710655" DDC="006.3/33" Normalized_DDC="006333" Normalized_Weight="0.2" />
</rec>
<rec ID="/54094.html" Type="incollection" CiteSeer_Book="Proceedings 1st Int Conf on Typed Lambda Calculi and Applications TLCA93 Utrecht The Netherlands 1618 March 1993" CiteSeer_Volume="" Title="Pure Type Systems Formalized,">
<identifier Org="ISBN:0198501277" Paper_ID="/54094.html" Extracted="0198501277" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:1402007493" Paper_ID="/54094.html" Extracted="1402007493" DDC="530.13/8" Normalized_DDC="530138" Normalized_Weight="0.0625" />
<identifier Org="ISBN:1581138504" Paper_ID="/54094.html" Extracted="1581138504" DDC="005.13/3" Normalized_DDC="005133" Normalized_Weight="0.0625" />
<identifier Org="ISBN:354021366X" Paper_ID="/54094.html" Extracted="354021366X" DDC="005.1/1" Normalized_DDC="00511" Normalized_Weight="0.0625" />
<identifier Org="ISBN:354040709X" Paper_ID="/54094.html" Extracted="354040709X" />
<identifier Org="ISBN:3540565175" Paper_ID="/54094.html" Extracted="3540565175" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540578269" Paper_ID="/54094.html" Extracted="3540578269" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540580859" Paper_ID="/54094.html" Extracted="3540580859" DDC="005.1/01/5113" Normalized_DDC="0051015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540584501" Paper_ID="/54094.html" Extracted="3540584501" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540605797" Paper_ID="/54094.html" Extracted="3540605797" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540615113" Paper_ID="/54094.html" Extracted="3540615113" DDC="006.3/3" Normalized_DDC="00633" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540633790" Paper_ID="/54094.html" Extracted="3540633790" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540633987" Paper_ID="/54094.html" Extracted="3540633987" DDC="005.13/3" Normalized_DDC="005133" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540651373" Paper_ID="/54094.html" Extracted="3540651373" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540657630" Paper_ID="/54094.html" Extracted="3540657630" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540665366" Paper_ID="/54094.html" Extracted="3540665366" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540679340" Paper_ID="/54094.html" Extracted="3540679340" DDC="346/.092" Normalized_DDC="346092" Normalized_Weight="0.0625" />
<identifier Org="ISBN:3540851097" Paper_ID="/54094.html" Extracted="3540851097" />
</rec>
<rec ID="/2835.html" Type="article" CiteSeer_Book="Journal of Automated Reasoning" CiteSeer_Volume="" Title="A Proof of the {Church}--{R}osser Theorem and its Representation in a Logical Framework," />
<rec ID="/343057.html" Type="phdthesis" CiteSeer_Book="" CiteSeer_Volume="" Title="The Theory of {LEGO}: {A} Proof Checker for the Extended Calculus of Constructions,">
<identifier Org="ISBN:0198501277" Paper_ID="/343057.html" Extracted="0198501277" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:1402006071" Paper_ID="/343057.html" Extracted="1402006071" DDC="004" Normalized_DDC="004" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:1402006993" Paper_ID="/343057.html" Extracted="1402006993" DDC="160" Normalized_DDC="16" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:1402007493" Paper_ID="/343057.html" Extracted="1402007493" DDC="530.13/8" Normalized_DDC="530138" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:354021366X" Paper_ID="/343057.html" Extracted="354021366X" DDC="005.1/1" Normalized_DDC="00511" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540307044" Paper_ID="/343057.html" Extracted="3540307044" DDC="511.3/6" Normalized_DDC="51136" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540314288" Paper_ID="/343057.html" Extracted="3540314288" DDC="005.131" Normalized_DDC="005131" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540418644" Paper_ID="/343057.html" Extracted="3540418644" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:354042525X" Paper_ID="/343057.html" Extracted="354042525X" DDC="004/.01/51" Normalized_DDC="0040151" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540425586" Paper_ID="/343057.html" Extracted="3540425586" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540440445" Paper_ID="/343057.html" Extracted="3540440445" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540442405" Paper_ID="/343057.html" Extracted="3540442405" DDC="005.1/01/5113" Normalized_DDC="0051015113" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540580859" Paper_ID="/343057.html" Extracted="3540580859" DDC="005.1/01/5113" Normalized_DDC="0051015113" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540605797" Paper_ID="/343057.html" Extracted="3540605797" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540610642" Paper_ID="/343057.html" Extracted="3540610642" DDC="511/.5" Normalized_DDC="5115" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540615113" Paper_ID="/343057.html" Extracted="3540615113" DDC="006.3/3" Normalized_DDC="00633" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540617809" Paper_ID="/343057.html" Extracted="3540617809" DDC="511.3/0285" Normalized_DDC="51130285" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540645896" Paper_ID="/343057.html" Extracted="3540645896" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540648275" Paper_ID="/343057.html" Extracted="3540648275" DDC="004" Normalized_DDC="004" Normalized_Weight="0.05263157894736842" />
<identifier Org="ISBN:3540926860" Paper_ID="/343057.html" Extracted="3540926860" />
</rec>
<rec ID="/68452.html" Type="inproceedings" CiteSeer_Book="Proceedings of the International Conference on Typed Lambda Calculi and Applications" CiteSeer_Volume="" Title="A Verified Typechecker,">
<identifier Org="ISBN:354021366X" Paper_ID="/68452.html" Extracted="354021366X" DDC="005.1/1" Normalized_DDC="00511" Normalized_Weight="0.25" />
<identifier Org="ISBN:3540283722" Paper_ID="/68452.html" Extracted="3540283722" />
<identifier Org="ISBN:3540605797" Paper_ID="/68452.html" Extracted="3540605797" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.25" />
<identifier Org="ISBN:3540610642" Paper_ID="/68452.html" Extracted="3540610642" DDC="511/.5" Normalized_DDC="5115" Normalized_Weight="0.25" />
<identifier Org="ISBN:3540651373" Paper_ID="/68452.html" Extracted="3540651373" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.25" />
</rec>
<rec ID="/153536.html" Type="incollection" CiteSeer_Book="TwentyFive Years of Constructive Type Theory" CiteSeer_Volume="" Title="How to Believe a Machine-Checked Proof,">
<identifier Org="ISBN:0198501277" Paper_ID="/153536.html" Extracted="0198501277" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:0262632950" Paper_ID="/153536.html" Extracted="0262632950" DDC="004/.2/1" Normalized_DDC="00421" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:1581137052" Paper_ID="/153536.html" Extracted="1581137052" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:3540645896" Paper_ID="/153536.html" Extracted="3540645896" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:3540651373" Paper_ID="/153536.html" Extracted="3540651373" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.16666666666666666" />
<identifier Org="ISBN:8876990747" Paper_ID="/153536.html" Extracted="8876990747" DDC="410" Normalized_DDC="41" Normalized_Weight="0.16666666666666666" />
</rec>
<rec ID="/76674.html" Type="phdthesis" CiteSeer_Book="" CiteSeer_Volume="" Title="Program Verification in Synthetic Domain Theory,">
<identifier Org="ISBN:0521580579" Paper_ID="/76674.html" Extracted="0521580579" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.3333333333333333" />
<identifier Org="ISBN:354063455X" Paper_ID="/76674.html" Extracted="354063455X" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.3333333333333333" />
<identifier Org="ISBN:3540659226" Paper_ID="/76674.html" Extracted="3540659226" DDC="004/.01/5113" Normalized_DDC="004015113" Normalized_Weight="0.3333333333333333" />
<identifier Org="ISBN:3826513525" Paper_ID="/76674.html" Extracted="3826513525" />
</rec>
<rec ID="/219937.html" Type="inproceedings" CiteSeer_Book="TAPSOFT97 Theory and Practice of Software Development" CiteSeer_Volume="" Title="Auxiliary Variables and Recursive Procedures,">
<identifier Org="ISBN:1402006071" Paper_ID="/219937.html" Extracted="1402006071" DDC="004" Normalized_DDC="004" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540442405" Paper_ID="/219937.html" Extracted="3540442405" DDC="005.1/01/5113" Normalized_DDC="0051015113" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540627812" Paper_ID="/219937.html" Extracted="3540627812" DDC="005.1/2" Normalized_DDC="00512" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540665374" Paper_ID="/219937.html" Extracted="3540665374" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.2" />
<identifier Org="ISBN:3540668365" Paper_ID="/219937.html" Extracted="3540668365" DDC="005" Normalized_DDC="005" Normalized_Weight="0.2" />
</rec>
<rec ID="SELF" Type="SELF" CiteSeer_Book="SELF" CiteSeer_Volume="SELF" Title="Some Lambda Calculus and Type Theory Formalized">
<identifier Org="ISBN:1581138504" Paper_ID="SELF" Extracted="1581138504" DDC="005.13/3" Normalized_DDC="005133" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540282319" Paper_ID="SELF" Extracted="3540282319" DDC="005.1/015113" Normalized_DDC="0051015113" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540314288" Paper_ID="SELF" Extracted="3540314288" DDC="005.131" Normalized_DDC="005131" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540403329" Paper_ID="SELF" Extracted="3540403329" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:354042525X" Paper_ID="SELF" Extracted="354042525X" DDC="004/.01/51" Normalized_DDC="0040151" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540654623" Paper_ID="SELF" Extracted="3540654623" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540744630" Paper_ID="SELF" Extracted="3540744630" />
<identifier Org="ISBN:3540745904" Paper_ID="SELF" Extracted="3540745904" DDC="005.1/15" Normalized_DDC="005115" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540787380" Paper_ID="SELF" Extracted="3540787380" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.1111111111111111" />
<identifier Org="ISBN:3540894381" Paper_ID="SELF" Extracted="3540894381" />
<identifier Org="ISBN:354093653X" Paper_ID="SELF" Extracted="354093653X" DDC="530.0148" Normalized_DDC="5300148" Normalized_Weight="0.1111111111111111" />
</rec>
</references_metadata>