A Type System for Certified Binaries ZHONGSHAOandVALERYTRIFONOV YaleUniversity BRATINSAHA IntelCorporation and NIKOLAOSPAPASPYROU NationalTechnicalUniversityofAthens A certified binary is a value together with a proof that the value satisfies a given specification. Existingcompilersthatgeneratecertifiedcodehavefocusedonsimplememoryandcontrol-flow safetyratherthanmoreadvancedproperties.Inthisarticle,wepresentageneralframeworkfor explicitlyrepresentingcomplexpropositionsandproofsintypedintermediateandassemblylan- guages.Thenewframeworkallowsustoreasonaboutcertifiedprogramsthatinvolveeffectswhile stillmaintainingdecidabletypechecking.Weshowhowtointegrateanentireproofsystem(the calculusofinductiveconstructions)intoacompilerintermediatelanguageandhowtheintermedi- atelanguagecanundergocomplextransformations(CPSandclosureconversion)whilepreserving proofsrepresentedinthetypesystem.Ourworkprovidesafoundationfortheprocessofautomat- icallygeneratingcertifiedbinariesinatype-theoreticframework. CategoriesandSubjectDescriptors:F.3.1[LogicsandMeaningsofPrograms]:Specifyingand VerifyingandReasoningaboutPrograms—Mechanicalverification;F.3.3[LogicsandMeanings ofPrograms]:StudiesofProgramConstructs—Typestructure GeneralTerms:Languages,Verification AdditionalKeyWordsandPhrases:Certifiedcode,proof-preservingcompilation,typedintermedi- atelanguages A preliminary version of this article appeared in the Proceedings of the 29th ACM SIGPLAN- SIGACTSymposiumonPrinciplesofProgrammingLanguages(POPL’02). ThisworkwassupportedinpartbyDARPAOASISgrantF30602-99-1-0519,NationalScienceFoun- dation(NSF)grantCCR-9901011,NSFITRgrantCCR-0081590,andNSFgrantCCR-0208618. Anyopinions,findings,andconclusionscontainedinthisarticlearethoseoftheauthorsanddo notreflecttheviewsoftheseagencies. Authors’ addresses: Z. Shao and V. Trifonov, Department of Computer Science, Yale University, P.O.Box208285,NewHaven,CT06520;email:{shao,trifonov}@cs.yale.edu;B.Saha,Micropro- cessorTechnologyLab,IntelCorporation,SantaClara,CA95054;email:[email protected]; N. Papaspyrou, National Technical University of Athens, Department of Electrical and Com- puter Engineering, Software Engineering Laboratory, 15780 Zografou, Athens, Greece; email: [email protected]. Permissiontomakedigitalorhardcopiesofpartorallofthisworkforpersonalorclassroomuseis grantedwithoutfeeprovidedthatcopiesarenotmadeordistributedforprofitordirectcommercial advantageandthatcopiesshowthisnoticeonthefirstpageorinitialscreenofadisplayalong withthefullcitation.CopyrightsforcomponentsofthisworkownedbyothersthanACMmustbe honored.Abstractingwithcreditispermitted.Tocopyotherwise,torepublish,topostonservers, toredistributetolists,ortouseanycomponentofthisworkinotherworksrequirespriorspecific permissionand/orafee.PermissionsmayberequestedfromPublicationsDept.,ACM,Inc.,1515 Broadway,NewYork,NY10036USA,fax:+1(212)869-0481,[email protected]. (cid:1)C 2005ACM0164-0925/05/0100-0001$5.00 ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005,Pages1–45. 2 • Z.Shaoetal. 1. INTRODUCTION Proof-carryingcode(PCC),aspioneeredbyNeculaandLee[1996]andNecula [1997], allows a code producer to provide a machine-language program to a host, along with a formal proof of its safety. The proof can be mechanically checkedbythehost;theproducerneednotbetrustedbecauseavalidproofis incontrovertibleevidenceofsafety. ThePCCframeworkisgeneralbecauseitcanbeappliedtocertifyarbitrary dataobjectswithcomplexspecifications[Necula1998;AppelandFelten2001]. For example, the Foundational PCC system [Appel and Felty 2000] can cer- tifyanypropertyexpressibleinChurch’shigher-orderlogic.Harper[2000]and Burstall and McKinna [1991] call all these proof-carrying constructs certified binaries(ordeliverables).Acertifiedbinaryisavalue(whichcanbeafunction, adatastructure,oracombinationofboth)togetherwithaproofthatthevalue satisfiesagivenspecification. Unfortunately, little is known on how to construct or generate certified bi- naries. Most existing certifying compilers [Necula and Lee 1998; Colby et al. 2000]havefocusedonsimplememoryandcontrol-flowsafetyonly.Typedinter- mediatelanguages[HarperandMorrisett1995]andtypedassemblylanguages [Morrisettetal.1998]areeffectivetechniquesforautomaticallygeneratingcer- tifiedcode;however,noneofthesetypesystemscanrivaltheexpressivenessof theactualhigher-orderpredicatelogic(whichcouldbeusedinanyFoundational PCCsystem). Inthisarticle,wepresentatype-theoreticframeworkforconstructing,com- posing,andreasoningaboutcertifiedbinaries.Ourplanistousetheformulae- as-types principle [Howard 1980] to represent propositions and proofs in a general type system, and then to investigate their relationship with compiler intermediateandassemblylanguages.Weshowhowtointegrateanentireproof system(thecalculusofinductiveconstructions[Paulin-Mohring1993;Coquand and Huet 1988]) into an intermediate language, and how to define complex transformations(CPSandclosureconversion)ofprogramsinthislanguageso thattheypreserveproofsrepresentedinthetypesystem.Ourapproachbuilds upon a large body of previous work in the logic and theorem-proving commu- nity (see Barendregt and Geuvers [1999] and Barendregt [1991] for a good summary),andmakesthefollowingnewcontributions: —Weshowhowtodesignnewtypedintermediatelanguagesthatarecapable ofrepresentingandmanipulatingpropositionsandproofs.Inparticular,we show how to maintain decidability of typechecking when reasoning about certifiedprogramsthatinvolveeffects.Thisisdifferentfromtheworkdone inthelogiccommunitywhichfocusesonstronglynormalizing(primitivere- cursive)programs. —We maintain a phase distinction between compile-time typechecking and run-time evaluation. This property is often lost in the presence of depen- dent types (which are necessary for representing proofs in predicate logic). We achieve this by never having the type language (see Section 3) depen- dentonthecomputationlanguage(seeSection4).Proofsareinsteadalways representedatthetypelevelusingdependentkinds. ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. ATypeSystemforCertifiedBinaries • 3 —Weshowhowtousepropositionstoexpressprograminvariantsandhowto use proofs to serve as static capabilities. Following Xi and Pfenning [1999], we use singleton types [Hayashi 1991] to support the necessary interaction between the type and computation languages. We can assign an accurate typetouncheckedvector(orarray)access(seeSection4.3).XiandPfenning [1999]canachievethesameusingconstraintchecking,buttheirsystemdoes not support arbitrary propositions and (explicit) proofs, so it is less general thanours. —Weuseasingletypelanguagetotypecheckdifferentcompilerintermediate languages. This is crucial because it is impractical to have separate proof librariesforeachintermediatelanguage.Weachievethisbyusinginductive definitionstodefinealltypesusedtoclassifycomputationterms.Thisinturn nicely fits our work on (fully reflexive) intensional type analysis [Trifonov etal.2000]intoasinglesystem. —WeshowhowtoperformCPSandclosureconversiononourintermediatelan- guageswhilestillpreservingproofsrepresentedinthetypesystem.Existing algorithms [Morrisett et al. 1998; Harper and Lillibridge 1993; Minamide et al. 1996; Barthe et al. 1999] all require that the transformation be per- formed on the entire type language. This is impractical because proofs are largeinsize;transformingthemcanaltertheirmeaningsandbreaktheshar- ing among different languages. We present new techniques that completely solvetheseproblems(Sections5–6). —Our type language is a variant of the calculus of inductive constructions of Paulin-Mohring [1993] and Coquand and Huet [1988]. Following Werner [1994], we give rigorous proofs for its meta-theoretic properties (subject re- duction,strongnormalization,confluence,andconsistencyoftheunderlying logic).Wealsogivethesoundnessproofforoursamplecomputationlanguage. See Sections 3–4, the Appendix, and the companion technical report [Shao etal.2001]fordetails. As far as we know, our work is the first comprehensive study on how to incor- porate higher-order predicate logic (with inductive terms and predicates) into typed intermediate languages. Our results are significant because they open up many new exciting possibilities in the area of type-based language design and compilation. The fact that we can internalize a very expressive logic into our type system means that formal reasoning traditionally done at the meta levelcannowbeexpressedinsidetheactuallanguageitself.Forexample,much of the past work on program verification using Hoare-like logics may now be capturedandmadeexplicitinatypedintermediatelanguage. From the standpoint of type-based language design, recent work [Harper and Morrisett 1995; Xi and Pfenning 1999; Crary et al. 1999; Walker 2000; CraryandWeirich2000;Trifonovetal.2000]hasproducedmanyspecialized, increasinglycomplextypesystems, eachwithitsownmeta-theoreticalproofs, yet it is unclear how they will fit together. We can hope to replace them with oneverygeneraltypesystemwhosemetatheoryisprovedonceandforall,and thatallowsthedefinitionofspecializedtypeoperatorsviathegeneralmecha- nism of inductive definitions. For example, inductive definitions subsume and ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. 4 • Z.Shaoetal. Fig.1. Typedλ-calculi—Askeleton. generalizeearliersystemsforintensionaltypeanalysis[HarperandMorrisett 1995;CraryandWeirich1999;Trifonovetal.2000]. We have a prototype implementation of our new type system in the FLINT compiler [Shao 1997; Shao et al. 1998], but making the implementation real- istic still involves solving many remaining problems (e.g., efficient proof rep- resentations). Nevertheless, we believe our current contributions constitute a significant step toward the goal of providing a practical end-to-end compiler thatgeneratescertifiedbinaries. 2. APPROACH Ourmainobjectivesaretodesigntypedintermediateandlow-levellanguages thatcandirectlymanipulatepropositionsandproofs,andthentousethemto certify realistic programs. We want our type system to be simple but general; wealsowanttosupportcomplextransformations(CPSandclosureconversion) thatpreserveproofsrepresentedinthetypesystem.Inthissection,wedescribe the main challenges involved in achieving these goals and give a high-level overviewofourmaintechniques. Before diving into the details, we first establish a few naming conventions that we will use in the rest of this article. Typed intermediate languages are usuallystructuredinthesamewayastypedλ-calculi.Figure1givesafragment of a richly typed λ-calculus, organized into four levels: kind schema (kscm) u, kind κ, type τ, and expression (exp) e. If we ignore kind schema and other ex- tensions,thisisjustthehigher-orderpolymorphicλ-calculus Fω [Girard1972]. We divide each typed intermediate language into a type sub-language and a computation sub-language. The type language contains the top three levels. Kindschemasclassifykindtermswhilekindsclassifytypeterms.Weoftensay thatakindtermκ haskindschemau,oratypetermτ haskindκ.Weassume allkindsusedtoclassifytypetermshavekindschemaKind,andalltypesused to classify expressions have kind (cid:5). Both the function type τ → τ and the 1 2 polymorphic type ∀t:κ.τ have kind (cid:5). Following the tradition, we sometimes say“akindκ”toimplythatκ haskindschemaKind,“atypeτ”toimplythatτ haskind(cid:5),and“atypeconstructorτ”toimplythatτ haskind“κ→ ···→(cid:5).” Kindtermswithotherkindschemas,ortypetermswithotherkindsarestrictly referredtoas“kindterms”or“typeterms.” The computation language contains just the lowest level, which is where we write the actual program. This language will eventually be compiled into ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. ATypeSystemforCertifiedBinaries • 5 machine code. We often use names such as computation terms, computation values,andcomputationfunctionstorefertovariousconstructsatthislevel. 2.1 RepresentingPropositionsandProofs Thefirststepistorepresentpropositionsandproofsforaparticularlogicina type-theoreticsetting.Themostestablishedtechniqueistousetheformulae-as- types principle (a.k.a. the Curry–Howard correspondence) [Howard 1980] to mappropositionsandproofsintoatypedλ-calculus.Theessentialidea,which isinspiredbyconstructivelogic,istousetypes(ofkind(cid:5))torepresentpropo- sitions,andexpressionstorepresentproofs.Aproofofanimplication P⊃Q is a function object that yields a proof of proposition Q when applied to a proof of proposition P. A proof of a conjunction P ∧ Q is a pair (e ,e ) such that e 1 2 1 is a proof of P and e is a proof of Q. A proof of disjunction P ∨ Q is a pair 2 (b,e)—ataggedunion—wherebiseither0or1andifb=0,theneisaproofof P; if b=1 then e is a proof of Q. There is no proof for the false proposition. A proofofauniversallyquantifiedproposition∀x∈B.P(x)isafunctionthatmaps everyelementbofthedomain Bintoaproofof P(b)where P isaunarypredi- cateonelementsof B.Finally,aproofofanexistentiallyquantifiedproposition ∃x∈B.P(x)isapair(b,e)wherebisanelementof Bandeisaproofof P(b). Proof-checking in the logic now becomes typechecking in the corresponding typed λ-calculus. There has been a large body of work done along this line in thelast30years;mosttype-basedproofassistantsarebasedonthisfundamen- tal principle. Good surveys of the previous work in this area can be found in Barendregt[1991]andBarendregtandGeuvers[1999]. 2.2 RepresentingCertifiedBinaries Under the type-theoretic setting, a certified binary S is just a pair (v,e) that consistsof: —a value v of type τ where v could be a function, a data structure, or any combinationofboth;and —aproofeof P(v)where P isaunarypredicateonelementsoftypeτ. HereeisjustanexpressionwithtypeP(v).ThepredicateP isadependenttype constructorwithkindτ→(cid:5).TheentirepackageShasadependentstrong-sum type(cid:6)x:τ.P(x). For example, suppose Nat is the domain for natural numbers and Prime is a unary predicate that asserts an element of Nat as a prime number; we introduce a type nat representing Nat, and a type constructor prime (of kind nat→(cid:5)) representing Prime. We can build a certified prime-number package bypairingavaluev(anaturalnumber)withaproofforthepropositionprime(v); theresultingcertifiedbinaryhastype (cid:6)x:nat.prime(x). Function values can be certified in the same way. Given a function f that takesanaturalnumberandreturnsanotheroneastheresult(i.e., f hastype nat → nat),inordertoshowthat f alwaysmapsaprimetoanotherprime,we ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. 6 • Z.Shaoetal. needaproofforthefollowingproposition: ∀x∈Nat.Prime(x)⊃Prime(f(x)). In a typed setting, this universally quantified proposition is represented as a dependentproducttype: (cid:7)x:nat.prime(x)→prime(f(x)). Theresultingcertifiedbinaryhastype (cid:6)f :nat→nat.(cid:7)x:nat.prime(x)→prime(f(x)). Herethetypeisnotonlydependentonvaluesbutalsoonfunctionapplications suchas f(x),soverifyingthecertifiedbinary,whichinvolvestypecheckingthe proof,inturnrequiresevaluatingtheunderlyingfunctionapplication. 2.3 TheProblemswithDependentTypes Theaboveschemeunfortunatelyfailstoworkinthecontextoftypedinterme- diate(orassembly)languages.Thereareatleastfourproblemswithdependent types;thethirdandfourtharepresenteveninthegeneralcontext. First,realprogramsofteninvolveeffectssuchasassignment,I/O,ornonter- mination. Effects interact badly with dependent types. In our previous exam- ple,supposethefunction f doesnotterminateoncertaininputs;thenclearly, typechecking—whichcouldinvolveapplying f—wouldbecomeundecidable.It ispossibletousetheeffectdiscipline[SheldonandGifford1990]toforcetypesto be dependent on pure computation only, but this does not work in some typed λ-calculi; for example, a “pure” term in Girard’s λU [Girard 1972] could still diverge. Even if applying f does not involve any effects, we still have more serious problems. In a type-preserving compiler, the body of the function f has to be compiled down to typed low-level languages. A few compilers perform typed CPSconversion[Morrisettetal.1998],butinthepresenceofdependenttypes, this is a very difficult problem [Barthe et al. 1999]. Also, typechecking in low- levellanguageswouldnowrequireperformingtheequivalentofβ-reductionson thelow-level(assembly)code;thisisawkwardanddifficulttosupportcleanly. Third,itisimportanttomaintainaphasedistinctionbetweencompile-time typecheckingandrun-timeevaluation.Buthavingdependentstrong-sumand producttypesmakesithardertopreservethisproperty,especiallyifthetype- dependentvaluesarefirst-classcitizens(certifiedbinariesareusedtovalidate arbitrary data structures and program functions so they should be allowed to bepassedasarguments,returnedasresults,orstoredinmemory). Finally, supporting subset types in the presence of dependent strong-sum andproducttypesisdifficultifnotimpossible[Constable1985;Nordstrometal. 1990]. A certified binary of type (cid:6)x:nat. prime(x) contains a natural number v andaproofthatvisaprime.However,inmanycases,wejustwantvtobelong to a subset type {x:nat | prime(x)}, that is, v is a prime number but the proof of this is not together with v; instead, it can be constructed from the current context. ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. ATypeSystemforCertifiedBinaries • 7 2.4 SeparatingtheTypeandComputationLanguages Wesolvetheseproblemsbymakingsurethatourtypelanguageisneverdepen- dent on the computation language. Because the actual computation term has tobecompileddowntoassemblycodeinanycase,itisabadideatotreatitas partoftypes.Thisseparationimmediatelygivesusbackthephase-distinction property. Torepresentpropositionsandproofs,welifteverythingonelevelup:weuse kinds to represent propositions, and type terms for proofs. The domain Nat is represented by a kind Nat; the predicate Prime is represented by a dependent kind term Prime which maps a type term of kind Nat to a proposition. A proof forpropositionPrime(n)certifiesthatthetypetermnisaprimenumber. To maintain decidable typechecking, we insist that the type language is stronglynormalizingandfreeofsideeffects.Thisispossiblebecausethetype language no longer depends on any runtime computation. Given a type-level function g ofkindNat→Nat,wecancertifythatitalwaysmapsaprimetoan- otherprimebybuildingaproofτ forthefollowingproposition,nowrepresented p asadependentproductkind: (cid:7)t:Nat.Prime(t)→Prime(g(t)). Essentially, we circumvent the problems with dependent types by replacing them with dependent kinds and by lifting everything (in the proof language) onelevelup. Toreasonaboutactualprograms,westillhavetoconnecttermsinthetype language with those in the computation language. We follow Xi and Pfenning [1999]andusesingletontypes[Hayashi1991]torelatecomputationvaluesto typeterms.Inthepreviousexample,weintroduceasingletontypeconstructor snat ofkindNat→(cid:5).GivenatypetermnofkindNat,ifacomputationvaluev hastypesnat(n),thenvdenotesthenaturalnumberrepresentedbyn. Acertifiedbinaryforaprimenumbernowcontainsthreeparts:atypetermn ofkindNat,aproofforthepropositionPrime(n),andacomputationvalueoftype snat(n).Wecanpackitupintoanexistentialpackageandmakeitafirst-class valuewithtype: ∃n:Nat.∃t:Prime(n).snat(n). Hereweuse∃ratherthan(cid:6) toemphasizethattypesandkindsarenolonger dependent on computation terms. Under the erasure semantics [Crary et al. 1998],thiscertifiedbinaryisjustanintegervalueoftypesnat(n)atruntime. Becausetherearestrongseparationbetweentypesandcomputationterms, a value v of type ∃n:Nat.∃t :Prime(n).snat(n) is still implemented as a single integeratruntimethusachievingtheeffectofthesubsettype. We can also build certified binaries for programs that involve effects. Re- turningtoourexample,assumeagainthat f isafunctioninthecomputation languagewhichmaynotterminateonsomeinputs.Supposewewanttocertify thatiftheinputto f isaprime,andthecallto f doesreturn,thentheresultis alsoaprime.Wecanachievethisintwosteps.First,weconstructatype-level function g ofkindNat→Nattosimulatethebehaviorof f (onallinputswhere ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. 8 • Z.Shaoetal. f doesterminate)andshowthat f hasthefollowingtype: ∀n:Nat.snat(n)→snat(g(n)). HerefollowingFigure1,weuse∀and→todenotethepolymorphicandfunction types for the computation language. The type for f says that if it takes an integeroftypesnat(n)asinputanddoesreturn,thenitwillreturnaninteger oftypesnat(g(n)).Second,weconstructaproofτ showingthat g alwaysmaps p a prime to another prime. The certified binary for f now also contains three parts: the type-level function g, the proof τ , and the computation function f p itself.Wecanpackitintoanexistentialpackagewithtype: ∃g:Nat→Nat.∃p:((cid:7)t:Nat.Prime(t)→Prime(g(t))). ∀n:Nat.snat(n)→snat(g(n)). Notice this type also contains function applications such as g(n), but g is a type-level function which is always strongly normalizing, so typechecking is stilldecidable. Itisimportanttounderstandthedifferencebetweentypecheckingand“type inference.”Themainobjectiveofthispaperistodevelopafullyexplicitframe- work where proofs and assertions can be used to certify programs that may contain side effects—the most important property is that typechecking (and proof-checking) in the new framework must be decidable. Type inference (i.e., findingtheproofs),ontheotherhand,couldbeundecidable:givenanarbitrar- ily complex function f, we clearly cannot hope to automatically construct the corresponding g. In practice, however, it is often possible to first write down the specification g and then to write the corresponding program f. Carrying outthisstepandconstructingtheproofthat f follows g isachallengingtask, asinanyotherPCCsystem[Necula1998;AppelandFelty2000]. 2.5 DesigningtheTypeLanguage Wecanincorporatepropositionsandproofsintotypedintermediatelanguages, but designing the actual type language is still a challenge. For decidable typechecking, the type language should not depend on the computation lan- guage and it must satisfy the usual meta-theoretical properties (e.g., strong normalization). But the type language also has to fulfill its usual responsibilities. First, it must provide a set of types (of kind (cid:5)) to classify the computation terms. A typicalcompilerintermediatelanguagesupportsalargenumberofbasictype constructors (e.g., integer, array, record, tagged union, and function). These typesmaychangetheirformsduringcompilation,sodifferentintermediatelan- guagesmayhavedifferentdefinitionsof(cid:5);forexample,acomputationfunction at the source level may be turned into CPS-style, or later, to one whose argu- ments are machine registers [Morrisett et al. 1998]. We also want to support intensionaltypeanalysis[HarperandMorrisett1995]whichiscrucialfortype- checkingruntimeservices[Monnieretal.2001]. Our solution is to provide a general mechanism of inductive definitions in our type language and to define each such (cid:5) as an inductive kind. This was ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. ATypeSystemforCertifiedBinaries • 9 made possible only recently [Trifonov et al. 2000] and it relies on the use of polymorphic kinds. Taking the type language in Figure 1 as an example, we add kind variables k and polymorphic kinds (cid:7)k :u.κ, and replace (cid:5) and its associatedtypeconstructorswithinductivedefinitions(notshown): (kscm) u::=Kind|... (kind) κ ::=κ →κ |k |(cid:7)k:u.κ |... 1 2 (type) τ ::=t |λt:κ.τ |τ τ |λk:u.τ |τ[κ]|... 1 2 Atthetypelevel,weaddkindabstractionλk:u.τ andkindapplicationτ[κ]. The kind (cid:5) is now inductively defined as follows (see Sections 3–4 for more details): Inductive(cid:5) : Kind :=→→: (cid:5)→(cid:5)→(cid:5) |∀∀ : (cid:7)k:Kind.(k→(cid:5))→(cid:5) . . . Here→→and∀∀aretwooftheconstructors(of(cid:5)).Thepolymorphictype∀t:κ.τ isnowwrittenas∀∀[κ](λt:κ.τ);thefunctiontypeτ →τ isjust→→τ τ . 1 2 1 2 Inductive definitions also greatly increase the programming power of our type language. We can introduce new data objects (e.g., integers, lists) and defineprimitiverecursivefunctions,allatthetypelevel;theseinturnareused tohelpmodelthebehaviorsofthecomputationterms. To have the type language double up as a proof language for higher-order predicatelogic,weadddependentproductkind(cid:7)t:κ .κ ,whichsubsumesthe 1 2 arrow kind κ →κ ; we also add kind-level functions to represent predicates. 1 2 Thus the type language naturally becomes the calculus of inductive construc- tions[Paulin-Mohring1993]. 2.6 Proof-PreservingCompilation Evenwithaproofsystemintegratedintoourintermediatelanguages,westill have to make sure that they can be CPS- and closure-converted down to low- level languages. These transformations should preserve proofs represented in the type system; in fact, they should not traverse the proofs at all since doing soisimpracticalwithlargeprooflibraries. Thesechallengesarenontrivialbutthewaywesetupourtypesystemmakes it easier to solve them. First, because our type language does not depend on the computation language, we do not have the difficulties involved in CPS- converting dependently typed λ-calculi [Barthe et al. 1999]. Second, all our intermediatelanguagessharethesametypelanguage,thusalsothesameproof library;thisispossiblebecausethe(cid:5)kind(andtheassociatedtypes)foreach intermediatelanguageisjustaregularinductivedefinition. Finally,atype-preservingprogramtransformationoftenrequirestranslating the source types (of the source (cid:5) kind) into the target types (of the target (cid:5) kind).ExistingCPS-andclosure-conversionalgorithms[Morrisettetal.1998; HarperandLillibridge1993;Minamideetal.1996]allperformthistranslation at the meta-level; they have to go through every type term (thus every proof terminoursetting)duringthetranslation,becauseanytypetermmaycontain a sub term that has the source (cid:5) kind. In our framework, the fact that each ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005. 10 • Z.Shaoetal. (cid:5) kind is inductively defined means that we can internalize and write the type-translationfunctioninsideourtypelanguageitself.Thisleadstoelegant algorithms that do not traverse any proof terms but still preserve typing and proofs(seeSections5–6fordetails). 2.7 PuttingItAllTogether Acertifyingcompilerinourframeworkwillhaveaseriesofintermediatelan- guages, each corresponding to a particular stage in the compilation process; all will share the same type language. An intermediate language is now just the type language plus the corresponding computation terms, along with the inductivedefinitionforthecorresponding(cid:5)kind.Intherestofthisarticle,we firstgiveaformaldefinitionofourtypelanguage(whichwillbenamedTLfrom now on) in Section 3; we then present a sample computation language λ in H Section 4; we show how λ can be CPS- and closure-converted into low-level H languagesinSections5–6;finally,wediscussrelatedworkandthenconclude. 3. THETYPELANGUAGETL Our type language TL resembles the calculus of inductive constructions (CIC) implemented in the Coq proof assistant [Huet et al. 2000]. This is a great ad- vantage because Coq is a very mature system and it has a large set of proof librarieswhichwecanpotentiallyreuse.Forthisarticle,wedecidednottodi- rectlyuseCICasourtypelanguageforthreereasons.First,CICcontainssome featuresdesignedforprogramextraction[Paulin-Mohring1989],whicharenot requiredinourcase(whereproofsareonlyusedasspecificationsforthecom- putation terms). Second, as far as we know, there are still no formal studies covering the entire CIC language. Third, for theoretical purposes, we want to understand what are the most essential features for modeling certified bina- ries.Inpractice,thesedifferencesarefairlyminor.Themainobjectivesofthis section is to give a quick introduction to the essential features in the Coq-like dependenttypetheory. 3.1 Motivations FollowingthediscussioninSection2.5,weorganizeTLintothefollowingthree levels: (kscm) u::=z |(cid:7)t:κ.u|(cid:7)k:u.u(cid:9) |Kind (kind) κ ::=k |λt:κ.κ(cid:9) |κ[τ]|λk:u.κ |κκ(cid:9) |(cid:7)t:κ.κ(cid:9) |(cid:7)k:u.κ |(cid:7)z:Kscm.κ |Ind(k:Kind){κ(cid:10)}|Elim[κ(cid:9),u](τ){κ(cid:10)} (type) τ ::=t |λt:κ.τ |ττ(cid:9) |λk:u.τ |τ[κ]|λz:Kscm.τ |τ[u] |Ctor(i,κ)|Elim[κ(cid:9),κ](τ(cid:9)){τ(cid:10)} Herekindschemas(kscm)classifykindtermswhilekindsclassifytypeterms. Therearevariablesatallthreelevels:kind-schemavariablesz,kindvariables k, and type variables t. We have an external constant Kscm classifying all the kindschemas;essentially,TLhasanadditionallevelabovekscm,ofwhichKscm isthesolemember. ACMTransactionsonProgrammingLanguagesandSystems,Vol.27,No.1,January2005.