A List-machine Benchmark for Mechanized Metatheory

Description

LFMTP 2006
A List-machine Benchmark for
Mechanized Metatheory (Extended Abstract)
Andrew W. Appel
Princeton University and INRIA Rocquencourt
Xavier Leroy
INRIA Rocquencourt
Abstract
We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler
correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler imple-
mentations, and we point out that much can be done without binders or alpha-conversion. We propose
specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions
in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.
Keywords: Theorem proving, proof assistants, program proof, compiler verification, typed machine
language, metatheory, Coq, Twelf.
1 How to evaluate mechanized metatheories
The POPLmark challenge [3] aims to compare the usability of several automated
proof assistants for mechanizing the kind of programming-language proofs that
might be done by the author of a POPL paper, with benchmark problems “chosen
to exercise many aspects of programming languages that are known to be difficult
to formalize.” The first POPLmark examples are all in the theory of F and<:
emphasize the theory of binders (e.g., alpha-conversion).
Practitioners of machine-checked proof about real compilers have interests that
are similar but not identical. We want to formally relate machine-checked proofs
Ato actual ...

Sujets

• Lubine
• Nîlgîri
• Clauses du contrat de travail en France
• Branchie
• Fetchmail
• Instrument à anche

Informations

• Publié par: Fioz
• Nombre de lectures: 63
• Langue: English

Extrait

LFMTP2006 AList-machineBenchmarkfor MechanizedMetatheory (ExtendedAbstract) AndrewW.Appel PrincetonUniversityandINRIARocquencourt XavierLeroy INRIARocquencourt Abstract Weproposeabenchmarktocomparetheorem-provingsystemsontheirabilitytoexpressproofsofcompiler correctness.IncontrasttothefirstPOPLmark,weemphasizetheconnectionofproofstocompilerimple- mentations,andwepointoutthatmuchcanbedonewithoutbindersoralpha-conversion.Wepropose specificcriteriaforevaluatingtheutilityofmechanizedmetatheorysystems;wehaveconstructedsolutions inbothCoqandTwelfmetatheory,andwedrawconclusionsaboutthosetwosystemsinparticular. Keywords:Theoremproving,proofassistants,programproof,compilerverification,typedmachine language,metatheory,Coq,Twelf. 1Howtoevaluatemechanizedmetatheories ThePOPLmarkchallenge[3]aimstocomparetheusabilityofseveralautomated proofassistantsformechanizingthekindofprogramming-languageproofsthat mightbedonebytheauthorofaPOPLpaper,withbenchmarkproblems“chosen toexercisemanyaspectsofprogramminglanguagesthatareknowntobedifficult toformalize.”ThefirstPOPLmarkexamplesareallinthetheoryofF <: and emphasizethetheoryofbinders(e.g.,alpha-conversion). Practitionersofmachine-checkedproofaboutrealcompilershaveintereststhat aresimilarbutnotidentical.Wewanttoformallyrelatemachine-checkedproofs toactualimplementations,notparticularlytoLAT E Xdocuments.Furthermore, perhapsitisthewrongapproachto“exerciseaspects...thatareknowntobe difficulttoformalize.”Bindersandαβ-conversionarecertainlyuseful,butthey arenotessentialforprovingrealthingsaboutrealcompilers,asdemonstratedin severalsubstantialcompiler-verificationprojects[9,10,13,6,7,8].Ifmachine-checked proofistobeusefulinprovidingguaranteesaboutrealsystems,letusplaytoits strengths,nottoitsweaknesses. Thispaperiselectronicallypublishedin ElectronicNotesinTheoreticalComputerScience URL: www.elsevier.nl/locate/entcs

AppelandLeroy Thereforewehavedesignedadown-to-earthexampleofmachine-checkedmetathe- ory,closertothesemanticsoftypedassemblylanguages.Itisentirelyfirst-order, withoutbindersortheneedforalphaconversion.WespecifytheStructuredOper- ationalSemantics(SOS)ofasimplepointermachine(cons,car,cdr,branch-if-nil) andwepresentasimpletypesystemwithconstructorsforlist-of-τandnonempty- list-of-τ.Thebenchmarkexplicitlycoverstherelationshipofproofsaboutatype systemtoproofsaboutanexecutabletypechecker. Thechallengeistorepresentthetypesystem,provesoundnessofthetypesys- tem,representthetype-checkingalgorithm,andprovethatthealgorithmcorrectly implementsthetypesystem.WehaveimplementedthebenchmarkbothinCoq andinTwelfmetatheory,andwedrawconclusionsabouttheusabilityofthesetwo systems. Welackspacetopresenthere,butdiscussinthefullpaper[1], •howtheneedsofimplementors(ofprovablycorrectcompilersandprovablysound typecheckers)differfromtheneedsofPOPLauthorsaddressedbythefirst POPLmark; •aspecificationoftheentireproblemdowntodetailssuchastherecommended ascii namesforpredicatesandinferencerules; • detailsofourCoqandTwelfsolutions; •moredetailsaboutwhichsubtaskswereeasyordifficultinCoqandTwelf; •howeasyitistolearnTwelfandCoqgiventheavailabledocumentation. Aswellasabenchmark,thelistmachineisausefulexerciseforstudentslearning CoqorTwelf;wepresenttheoutlinesofoursolutions(withproofsdeleted)onthe Web[2]. 2Specificationoftheproblem Machinesyntax.MachinevaluesAareconscellsandnil. a:A::=nil | cons(a 1 ,a 2 ) Theinstructionsofthemachineareasfollows: ι:I::= jumpl(jumptolabell) | branch-if-nilvl(ifv=nilgotol) | fetch-fieldv0v 0 (fetchtheheadofvintov 0 ) | fetch-fieldv1v 0 (fetchthetailofvintov 0 ) | consv 0 v 1 v 0 (makeaconscellinv 0 ) | halt(stopexecuting) | ι 0 ;ι 1 (sequentialcomposition) Inthesyntaxabove,themetavariablesv i rangeovervariables;thevariablesthem- selvesv i areenumeratedbythenaturalnumbers.Similarly,metavariablesl i range overprogramlabelsL i . Aprogramisasequenceofinstructionblocks,eachprecededbyalabel. p:P::=L n :ι;p | end 2

AppelandLeroy Operationalsemantics.Machinestatesarepairs(r,ι)ofthecurrentinstruction ιandastorerassociatingvaluestovariables.Wewriter(v)=atomeanthata isthevalueofvariablevinr,andr[v:=a]=r 0 tomeanthatupdatingrwiththe binding[v:=a]yieldsauniquestorer 0 .Thesemanticsofthemachineisdefined p bythesmall-steprelation(r,ι) 7→ (r 0 ,ι 0 )definedbytherulesbelow,andtheKleene p closureofthisrelation,(r,ι) 7→ ∗ (r 0 ,ι 0 ). p (r,(ι 1 ;ι 2 );ι 3 ) 7→ (r,ι 1 ;(ι 2 ;ι 3 )) r(v)=cons(a 0 ,a 1 )r[v 0 :=a 0 ]=r 0 r(v)=cons(a 0 ,a 1 )r[v 0 :=a 1 ]=r 0 pp (r,(fetch-fieldv0v 0 ;ι)) 7→ (r 0 ,ι)(r,(fetch-fieldv1v 0 ;ι)) 7→ (r 0 ,ι) r(v 0 )=a 0 r(v 1 )=a 1 r[v 0 :=cons(a 0 ,a 1 )]=r 0 p (r,(consv 0 v 1 v 0 ;ι)) 7→ (r 0 ,ι) r(v)=cons(a 0 ,a 1 )r(v)=nilp(l)=ι 0 pp (r,(branch-if-nilvl;ι)) 7→ (r,ι)(r,(branch-if-nilvl;ι)) 7→ (r,ι 0 ) p(l)=ι 0 p (r,jumpl) 7→ (r,ι 0 ) Aprogrampruns,thatis,p ⇓ ,ifitexecutesfromaninitialstatetoafinalstate. Astateisaninitialstateifvariablev 0 =nilandthecurrentinstructionistheone atL 0 .Astateisafinalstateifthecurrentinstructionishalt. p {} [v 0 :=nil]=rp(L 0 )=ι(r,ι) 7→ ∗ (r 0 ,halt) ⇓ p Itisusefulforabenchmarkformachine-verifiedprooftoincludeexplicit ascii namesforeachconstructorandrule.Ourfullspecification[1]doesthat. Atypesystem.Wewillassigntoeachlivevariableateachprogrampointalist type.Toguaranteesafetyofcertainoperations,weproviderefinementsofthelist typefornonemptylistsandforemptylists.Inparticular,thefetch-fieldoperations demandthattheirlistargumenthasnonemptylisttype,andthebranch-if-nil operationrefinesthetypeofitsargumenttoemptyornonemptylist,dependingon whetherthebranchistaken. τ:T::= nil(singletontypecontainingnil) | listτ(listwhoseelementshavetypeτ) | listconsτ(non-nillistofτ) AnenvironmentΓisantypeassignmentoftypestoasetofvariables.Wedefine theobvioussubtypingτ ⊂ τ 0 amongthevariousrefinementsofthelisttype,using acommonsetoffirst-ordersyntacticrules,easilyexpressibleinmostmechanized metatheories.Weextendsubtypingwidthwiseanddepthwisetoenvironments. Wedefinetheleastcommonsupertypeτ 1 u τ 2 =τ 3 oftwotypesτ 1 andτ 2 asthe smallestτ 3 suchthatτ 1 ⊂ τ 3 andτ 1 ⊂ τ 2 . Intheoperationalsemantics,aprogramisasequenceoflabeledbasicblocks.In ourtypesystem,aprogram-typing,rangedoverbyΠ,associatestoeachprogram labelavariable-typingenvironment.WewriteΠ(l)=ΓtoindicatethatΓrepresents thetypesofthevariablesonentrytotheblocklabeledl. 3

AppelandLeroy Instructiontypings.IndividualinstructionsaretypedbyajudgmentΠ ` instr Γ { ι } Γ 0 .Theintuitionisthat,underprogram-typingΠ,theHoaretripleΓ { ι } Γ 0 relatespreconditionΓtopostconditionΓ 0 . Π ` instr Γ { ι 1 } Γ 0 Π ` instr Γ 0 { ι 2 } Γ 00 Π ` instr Γ { ι 1 ;ι 2 } Γ 00 Γ(v)=listτΠ(l)=Γ 1 Γ[v:=nil]=Γ 0 Γ 0 ⊂ Γ 1 Π ` instr Γ { branch-if-nilvl } (v:listconsτ,Γ 0 ) Γ(v)=listconsτΠ(l)=Γ 1 Γ[v:=nil]=Γ 0 Γ 0 ⊂ Γ 1 Π ` instr Γ { branch-if-nilvl } Γ Γ(v)=nilΠ(l)=Γ 1 Γ ⊂ Γ 1 Π ` instr Γ { branch-if-nilvl } Γ Γ(v)=listconsτΓ[v 0 :=τ]=Γ 0 Γ(v)=listconsτΓ[v 0 :=listτ]=Γ 0 Π ` instr Γ { fetch-fieldv0v 0 } Γ 0 Π ` instr Γ { fetch-fieldv1v 0 } Γ 0 Γ(v 0 )=τ 0 Γ(v 1 )=τ 1 (listτ 0 ) u τ 1 =listτΓ[v:=listconsτ]=Γ 0 Π ` instr Γ { consv 0 v 1 v } Γ 0 Blocktypings.Ablockisaninstructionthatdoesnot(statically)continuewith anotherinstruction,becauseitendswithajump. Π ` instr Γ { ι 1 } Γ 0 Π;Γ 0 ` block ι 2 Π(l)=Γ 1 Γ ⊂ Γ 1 Π;Γ ` block ι 1 ;ι 2 Π;Γ ` block jumpl Programtypings.Wewrite | = prog p:Πandsaythataprogramphasprogram- typingΠifforeachlabeledblockl:ιinp,theblockιhasthepreconditionΠ(l)=Γ giveninΠ,thatis,Π;Γ ` block ι.Moreover,wedemandthatΠ(L 0 )=v 0 :nil, {} andthateverylabelldeclaredinΠisdefinedinp. Typesystemvs.typechecker.Wehavepresentedsomerelationsdefinedby derivationrulesandsomedefinedinformally.Thisisabitsloppy,especiallywhere aderivationrulereferstoaninformallydefinedrelation;anysolutiontothebench- markmustformalizethis.Wewillusethenotation | = prog p:Πtomeanthat programphastypeΠinthe(notnecessarilyalgorithmic)typesystem,andthe notation ` prog p:Πtomeanthatp:Πisderivedinsomealgorithmictype-checker. Thefullpaper[1]outlinestwosuchalgorithmictype-checkers.Oneiswrittenin pseudo-codeandcorrespondstoatype-checkerimplementedinimperativeorfunc- tionalstyle.Theotherrefinesthederivationrulesgivenabovetomakethemfully syntax-directedandthereforeamenabletoanimplementationasalogicprogram. Sampleprogram.Thefollowinglist-machineprogramhasthreebasicblocks. Variablev 0 isinitializedtonilasprescribedbytheoperationalsemantics.Block 0initializesv 1 tothelistcons(nil,cons(nil,nil))andjumpstoblock1.Block1 isaloopthat,whilev 1 isnotnil,fetchesthetailofv 1 andcontinues.Thelast instructionofblock1isactuallydeadcode(neverreached).Block2istheloop exit,andhalts. p sample = L 0 :consv 0 v 0 v 1 ;consv 0 v 1 v 1 ;consv 0 v 1 v 1 ;jumpL 1 ; L 1 :branch-if-nilv 1 L 2 ;fetch-field1v 1 v 1 ;branch-if-nilv 0 L 1 ;jumpL 2 ; L 2 :halt; dne 4

AppelandLeroy Theprogramiswell-typedwith Π sample =L 0 :(v 0 :nil, {} ),L 1 :(v 0 :nil,v 1 :listnil, {} ),L 2 : {} , {} 3Mechanizationtasks Implementingthe“list-machine”benchmarkinamechanizedmetatheory(MM) comprisesthefollowingtasks: 1.RepresenttheoperationalsemanticsintheMM. 2.Derivethefactthatp sample ⇓ .TheMMshouldconvenientlysimulateexecution ofsmallexamples,sotheusercandebugtheSOSandgetanintuitivefeelfor itsexpressiveness. Soundnessofatypesystem. 3.RepresentthetypesystemintheMM(defineenoughnotationtorepresent theformula | = prog p:Πandinferencerulesfromwhichtype-soundesscouldbe proved). 4.RepresentintheMManalgorithmforleast-common-supertype,thatis,the computationτ 1 u τ 2 =τ 3 producingτ 3 frominputsτ 1 andτ 2 . 5.Usingthetypesystem,derivethefactthat | = prog p sample :Π sample .TheMM shouldconvenientlysimulatetype-checkingofsmallexamples,sotheusercan debugthetypesystemandgetafeelforitsexpressiveness. 6.Representthestatementofthedefiningpropertiesofleastcommonsupertypes, e.g.,τ 1 u τ 2 =τ 3 ⇒ τ 1 ⊂ τ 3 . 7.Provethatthe u algorithmenjoystheseproperties. 8.Representthestatementofasoundnesstheoremforthetypesystem.The informalstatementofsoundnessis,“awell-typedprogramwillnotgetstuck.” Aprogramstateisnotstuckifitstepsorhalts: p | = prog p:Πinitial(p,r,ι)(r,ι) 7→ ∗ (r 0 ,ι 0 ) ( ∃ r 00 ,ι 00 .(r 0 ,ι 0 ) 7→ p (r 00 ,ι 00 )) ∨ ι 0 =halt soundness 9.Provethesoundnesstheorem.Thefullpaper[1]outlinestheprincipallemmas ofthisproof,whichisastandardargumentbytypepreservationandprogress. Efficienttype-checkingalgorithm. 10.Representanasymptoticallyefficienttype-checkingalgorithm ` prog p:Πin theMM.ByefficientwemeanthatanN-instructionprogramwithMlive variablesshouldtype-checkinO(NlogM)time. 11.Usingthetype-checkingalgorithm,calculate ` prog p sample :Π sample .TheMM shouldsimulateexecutionofalgorithmsonsmallinputs. 12.Provethatthetype-checkingalgorithmterminatesonanyprogram. 13.Demonstratethetype-checkeronlarge-scaleexampleswithgoodperformance. TypicallythiswillbedonethroughanautomatictranslationtoPrologorML whichisthencompiledbyanoptimizingcompiler. 14.Provethat ` prog p:Πimplies | = prog p:Π.Thatis,thetype-checkersoundly implementsthetypesystem. 5

AppelandLeroy Writingthepaper. 15.UseanautomatictooltogeneratereadableLAT E XformulasfortheSOSrules, thetypingrules,andthestatementsof(nottheproofsof)theleast-common- supertypelemmasandsoundnesstheorems.KleinandNipkow[6]demonstrate thisverynicelyintheIsabelle/HOLformalizationofaJavasubsetcompiler. 4AproofinTwelfmetatheory TheTwelfsystem[12]isanimplementationoftheEdinburghLogicalFramework (LF).OnecanrepresenttheoperatorsofalogicastypeconstructorsinLF,and proofsinthatlogicastermsinLF,andonecandoproof-checkingbytype-checking theterms(consideringthemasderivations). InTwelfonecanprovetheorems(proofsinalogic),ormetatheorems(proofs aboutalogic).Eitherapproachcouldbeusedforourbenchmark.Oursolutionuses theusualapproachinTwelf,whichismetatheoretic. Inthiscasethelogicsinquestionareouroperationalsemanticsandourtype system,andthemetatheoremtobeprovedistypesoundness:thatis,ifonecan combinetheinferencerulesofthetypesystemtoproduceaderivationoftype- checking,thenitmustbepossibletocombinetheinferencerulesoftheSOSto produce(only)nonstuckderivationsofexecution. Thisapproachisagressivelysyntactic.Insteadofsayingthatpisamapping fromlabelstoinstructions,wegivesyntacticconstructionsthat(weclaim)represent suchamapping.Oneconsequenceofthisstyleisthatour | = prog p:Πisnotjusta semanticrelation,butasyntacticallyderivableoneexpressedasHornclauses.By carefullystructuringtheHornclausesthatdefineourrelationssothatwecaniden- tify“input”and“output”arguments,wecanensurethatthelogic-programming interpretationofourclausesisactuallyanalgorithm.Thisinput-outputorganiza- tioncanbespecifedandmechanicallycheckedinTwelfvia %mode declarations.Our typesystemisthendirectlyexecutableinTwelf. EachclauseinTwelfisnamed.WhenTwelftracesout,viaprolog-styleback- tracking,oneormorederivationsofaresultbythesuccessfulapplicationofclauses, itbuildsaswelladerivationtreeforeachderivation. InLF,onecancomputeaswellonthederivationtreesthemselves.Suppose wewriteanotherprologprogram(setofclauses)thattakesasinputaderivation treefortype-checking,andproducesasoutputaderivationtreeforsafe(nonstuck) execution.Ifthisprogramistotal(thatis,terminatessuccessfullyonanyinput) thenwehaveconstructivelyprovedthatanywelltypedprogramissafe. Toreasonaboutthismeta-program,weuse(machine-checked) %mode declara- tionstoexplainwhataretheinputsandoutputsofthederivationtransformer.We alsouse(machine-checked) %total declarationstoensurethatourmeta-program hascoveredallthecasesthatmayarise,andthatourmeta-programdoesnot infinite-loop.Wegiveanexampleofsuchaproofinsection6,items6and7. Twelfhasanamazingeconomyoffeatures.Onedoesnothavetolearnamodule system—becausethereisnone—onejustusesnamingconventionsonallone’siden- tifiers.Onedoesnothavetolearnhowtouselargelibrariesoflemmasandtactics, becausetherearenolibrariesoflemmasandtactics:butsuchlibrarieswouldnot 6

AppelandLeroy besouseful,becauseTwelfhasfewabstractionfeatures,andnopolymorphism.All proofsaredonewiththesimplemechanismofprovingthetotalityofmetaprograms. There’sacalculatedgamblehere:Inreturnforthebenefitofprovingeveryingin onesimplestyle,andrarelyhavingtotranslatebetweenabstractions,onetrades awaymanythings:therearesometheoremsthatthisnotationcannotevenexpress (becausethequantifiersarenestedtoodeep,forexample);andtherearesomethings thatareprovablebutinacontrivedway(expressingsemanticpropertiesonlywith inductivesyntacticconstructors),asillustratedbelow. OurTwelfproofstartsbydefininginductivelythenotionofequalitiesandin- equalitiesonnaturalnumbers,labels,variables,typestructure,andtermstructures. Wegivesyntacticcharacterizationsofwell-formedenvironments(i.e.,thatdonot mapthesamevariabletwice). Sometimesitistrickytomakeaproperlyinductivesyntacticdefinitionofa semanticproperty.Forexample,considerenvironmentsubtyping,semantically Γ 1 ⊂ env Γ 2 ≡∀ v.v ∈ domΓ 2 ⇒ (v ∈ domΓ 1 ∧ Γ 1 (v) ⊂ Γ 2 (v)). An“obvious”“inductive”definitionusesthesyntacticrules, Γ 1 (v)=τ 0 τ 0 ⊂ τΓ 1 ⊂ env Γ 2 a a 1 2 Γ ⊂{} Γ 1 ⊂ env v:τ,Γ 2 Theinductionis(supposedly)overthesizeofthetermtotherightofthe ⊂ env symbol.However,thisdefinitionisnotsufficientlyinductiveforusefulproperties (transitivity,reflexivity)tobeprovable—atleast,wewerenotabletoprovethem. TheproblemappearstobethatΓ 1 doesnotdecreaseinrulea 2 . Thefollowingdefinitionisproperlyinductive—weuseΓ 0 insteadofΓ 1 inthe premiseofruleb 2 .Provingtransitivityandreflexivityfromthisdefinitioniseasy; thedifficultyistoavoidwastingtimewiththepseudoinductivedefinitionabove. Γ 1 = . (v:τ 0 ,Γ 0 )τ 0 ⊂ τΓ 0 ⊂ env Γ 2 b Γ ⊂ env {} 1 Γ 1 ⊂ env v:τ,Γ 2 b 2 5AproofinCoq TheCoqsystem[5,4]isaproofassistantbasedontheCalculusofInductiveCon- structions.Thislogicisavariantoftypetheory,followingthe“propositions-as- types,proofs-as-terms”paradigm,enrichedwithbuilt-insupportforinductiveand coinductivedefinitionsofpredicatesanddatatypes. Fromauser’sperspective,Coqoffersarichspecificationlanguagetodefineprob- lemsandstatetheoremsaboutthem.Thislanguageincludes(1)constructivelogic withalltheusualconnectivesandquantifiers;(2)inductivedefinitionsviainference rulesandaxioms(asinTwelf’smeta-logic);(3)apurefunctionalprogramming languagewithpattern-matchingandstructuralrecursion(inthestyleofMLor Haskell). Forthelist-machinebenchmark,weusedacombinationofallthreespecification styles,followingcommonpracticeinresearchpapersontypesystems.Theinference rulesforoperationalsemanticsandthetypesystemsaretranscribeddirectlyas inductivedefinitions.Operationsoverstores,environmentsandprogram-typings, aswellasleastcommonsupertypesandthetype-checkingalgorithmarepresented 7

AppelandLeroy asfunctions.Finally,subtypingbetweenenvironmentsΓ ⊂ Γ 0 isdefinedbythe propositionalformula ∀ v, ∀ t 0 ,Γ 0 (v)=t 0 ⇒∃ t,Γ(v)=t ∧ t ⊂ t 0 UnlikeTwelf’smeta-theory,thelogicofCoqprovidesrichformsofpolymor- phism.Thisenabledustofactoroutthetreatmentofstores,environments,and program-typingsbyreusinganefficient,polymorphicimplementationoffinitemaps asradix-2searchtreesdevelopedearlierbyLeroyaspartoftheCompcertproject[8]. 6Comparisonofmechanizedproofs TaskTwelfCoq 1.OperationalSemantics12698lines 2.Derivep ⇓ 18 3.Typesystem | = prog p:Π167130 4. u algorithm** 5.Derive | = prog p sample :Π sample 1no 6.Statepropertiesof u 1213 7.Provepropertiesof u 11421 8.Statesoundnesstheorem2915 9.Provesoundnessof | = prog p:Pi2060315 10.Efficientalgorithm22145 11.Derive ` prog p sample :Π sample 11 12.Proveterminationof ` prog p:Π180 13.Scalabletype-checkeryesyes 14.Provesoundnessof ` prog p:Pi347141 15.GenerateLAT E Xnono WehaveimplementedthosetasksthatareimplementableinboththeTwelf (metatheory)andCoqsystems.Thenumberoflinesofcoderequiredissummarized inthetableabove.Totalparsingandproof-checkingtime 1 was0.558secondsreal timeforTwelf,2.622secondsforCoq. 1.Operationalsemantics.BothTwelfandCoqmakeiteasyandnatural torepresentinductivedefinitionsofthekindfoundinSOS.InCoqonealsohas thechoiceofrepresentingoperationsovermappings(e.g.,lookupandupdatein stores)eitherasrelations(definedbyinductivepredicates)orasfunctions(defined byrecursionandpattern-matching). 2.Derivep ⇓ .Twelfmakesitveryeasytointerpretinductivedefinitionsas logicprograms.ThereforethistaskwastrivialinTwelf.Coqdoesnotprovide ageneralmechanismtoexecuteinductivedefinitions.However,therulesforthe operationalsemanticsweresimpleenoughthat(aftersomeexperimentation)we couldusetheproofsearchfacilitiesofCoq(the eauto tactic)asapoorman’slogic programinterpreter.Amoregeneralmethodtoexecuteinductivedefinitionsin Coq,whichweimplementedalso,istodefineanexecutionfunction(61lines),prove itscorrectnesswithrespecttotheinductivedefinition(35lines),thenexecutethe function.(EvaluationoffunctionalprogramsissupportednativelybyCoq.) 1 DellPrecision360,Linux,2.8GHzPentium4,1GBRAM,512kBcache. 8

AppelandLeroy 3.Representthetypesystem.EasyandnaturalinbothTwelfandCoq (with,asbefore,thechoiceinCoqofusingthefunctionalpresentationofoperations overmappings). 4.Least-upper-boundalgorithm.Becausethe“typesystem”representedin Twelfismoststraightforwardlydoneasaconstructivealgorithm,thiswasalready doneaspartoftask3inourTwelfrepresentation.InCoq,whilethetypesystem itselfisnotalgorithmic,wechosetospecifytheleast-upperboundoperationasa functionfrompairsoftypestotypes.Therefore,thealgorithmtocomputeleast- upperboundswasalreadydoneaspartoftask3intheCoqdevelopmentaswell. 5.Deriveanexampleoftype-checking.TrivialtodoinTwelf,byrunning thetypesystemasalogicprogram.NotdirectlypossibleinCoqbecausethe specificationofthetypesystemisnotalgorithmic:itusesuniversalquantification overallvariablestospecifyenvironmentsubtyping. 6.Statepropertiesofleast-upper-bound.EntirelystraightforwardinCoq. Forexample,herearetheCoqstatementsoftheseproperties: Lemmalub_comm:forallt1t2,lubt2t1=lubt1t2. Lemmalub_subtype_left:forallt1t2,subtypet1(lubt1t2). Lemmalub_subtype_right:forallt1t2,subtypet2(lubt1t2). Lemmalub_least:forallt1t3,subtypet1t3-> forallt2,subtypet2t3->subtype(lubt1t2)t3. Thecorrespondencewiththemathematicalstatementsofthesepropertiesisobvi- .suo InTwelf,statingthepropertiesofleast-upper-boundmustbedoneinaway thatseemsartificialatfirst,butoncelearnedisreasonablynatural.Thelemma τ 1 u τ 2 =τ 3 lub-subtype-left τ ⊂ τ 31 isrepresentedasalogic-programmingpredicate, lub-subtype-left:lubT1T2T3->subtypeT1T3->type. whichtransformsaderivationof lubT1T2T3 intoaderivationof subtypeT1T3 . The“proof”willconsistoflogic-programmingclausesoverthispredicate.Tobea “proof”ofthepropertywewant,wewillhavetodemonstrate(tothesatisfaction ofthemetatheory,whichchecksourclaims)thatourclauseshavethefollowing properties: %modelub-subtype-left+P1-P2. Themodesofalogicprogramspecifywhich argumentsaretobeconsideredinputs( + )andwhichareoutputs( - ).For- mally,givenanygroundterm(i.e.,containingnologicvariables) P1 whosetypeis lubT1T2T3 ,ourclauses(iftheyterminate)mustproduceoutputs P2 oftype subtypeT1T3 thatarealsogroundterms. %totalP1(lub-subtype-leftP1P2). Weaskthemetatheoremtocheckour claimthatnoexecutionoflub-subtype-leftcaninfinite-loop:itmusteitherfail orproduceaderivationof subtypeT1T3 ;andwechecktheclaimthatthe executionneverfails(thatallcasesarecovered).Theuseof P1 intwoplaces inour %total declarationis(insomesense)mixingthethingtobeprovedwith partoftheproof:weindicatethattheinductionshouldbedoneoverargument 9