Design, Analysis and Reasoning about Tools Abstracts from the Third Workshop

Design,AnalysisandReasoningaboutTools:

AbstractsfromtheThirdWorkshop

FlemmingNielson

(editor)October1993

1Introduction

ThethirdDARTworkshoptookplaceonThursdayAugustl9thandFri-dayAugust20thattheDepartmentofComputerScience(DIKU)attheUniversityofCopenhagen;itwasorganizedbyMadsRosendahlandothersatDIKU,andTorbenAmtoftandSusanneBrønberghelpedproducingthisreport.Thefirstdaycomprisedsurveypresentationswhereasthesecondcontainedmoreresearchorientedtalks.TheprimaryaimoftheworkshopwastoincreasetheawarenessofDARTparticipantsforeachother’swork,tostimulatecollaborationbetweenthedifferentgroups,andtoinformDanishindustryabouttheskillspossessedbythegroups.

TheDARTprojectstartedinMarch1991(prematurelyterminatingasmallerprojectonFormalImplementation,TransformationandAnalysisofPrograms)andisfundedbytheDanishResearchCouncilsaspartoftheDanishResearchProgrammeonInformatics.Todateithasreceivedabout8millionDanishkronerinfundingforactivitiesgoingonatfourDanishinstitutions:TheDepartmentofComputerScienceatAarhusUniversity(UffeEngberg,PeterMosses,FlemmingNielson,HanneRiisNielson,MichaelSchwartzbach,GlynnWinskel,andothers);TheDepartmentofComputerScienceatCopenhagenUniversity(KlausGrue,FritzHenglein,NeilJones,TorbenMogensen,MadsRosendahl,MadsTofte,andothers);TheDepart-mentofComputerScienceatAalborgUniversityCentre(HansH¨uttel,Anna

1

Ingolfsdottir,KimLarsen,ArneSkou,andothers);TheDepartmentofCom-puterScienceatTheTechnicalUniversityofDenmark(BoHansen,PeterSestoft,andothers).ThisspringtheprojectunderwentinternationalreviewaspartofanoverallreviewoftheDanishResearchProgrammeonInformat-ics;copiesoftheevaluationreportareavailablefromtheDanishResearchCouncils.

Goalsoftheproject

Theapplicationanddevelopmentofformalmethodsisanintegralpartoftheresearchontheoreticalcomputerscience.Amaingoalofthisprojecthasbeentoactasacatalysttodevelopfurthercontactsamongtheworldsoftechniques,methodsandtoolsindifferentapplicationdomains.

AnincreasingawarenessthattechniquesandtoolsfromoneapplicationdomainareoftenrelevanttootherdomainsindicatesthatourprojectisofrelevancetoadvancedpartsofDanishindustry.

Itmaybeasomewhatidealgoaltoaimforallsoftwareandhardwaresystemstobevalidatedformally.However,theconceptof“safetycriticalsystems”hasbeencoinedtoclearlyidentifythosesystemswheresafetyisofparamountimportance;examplesincludetrafficcontrolsystemsforair-planes,trainsandcars,processcontrolatnuclearpowerstations,chemicalandbiologicalplantsetc.Performingsuchvalidationisdifficultpartlybe-causeofthesheersizeofrealisticapplicationsandpartlybecauseofalackoftools:languagessufficientlypowerfultoexpressreal-worldrequirements;programmingsystemstotransformspecificationsintosolutions;andsuffi-cientlypowerfulandautomatedvalidationtechniquestoprovethatagivensystemsatisfiesagivenspecification.

Thisprojectparticipatesininternationalactivitiesenhancingtheworldstate-of-the-artinmethods,toolsandtechniquestoensurethecorrectper-formanceofsystems.Amajorobjectiveisfullorpartialautomationoftasksaidingtheoverallgoalofproducingreliablesystemsthatarefaithfultothesemanticsofvariousapplicationareas,therebyfacilitatingthehandlingofmorethanjusttoyapplications.Thisnecessitatesastrongfoundationinse-manticsandmayrequirethedevelopmentoradaptationofnewtheories.Ouroverallapproachisappropriatesinceourmethodsarefirmlybasedonseman-ticfoundations.Techniqueswehaveemphasizedincludeautomatedtheorem

2

proving,programanalysis,andfullyautomaticprogramoptimizationandtransformationtechniques.Activitiesoftheproject

Almostallofouractivitiespresupposetheabilitytomakeasemanticdescrip-tionofthesystemunderscrutiny.ThelastdecadesofresearchhaveshowntheadventofDenotationalSemanticsandStructuralOperationalSeman-tics.Theidealsemanticdescriptionmethodmustbeuniversallyapplicable,itmustbeunderstandabletoprogrammersaswellasspecialists,itmustallowmodularityinsemanticdefinitionsandneedstoscaleupwell,anditmustsupportthestudyofprogramanalysesandtransformations.Noneoftheexistingframeworksfullyliveuptoallthesegoals.

OneoftheactivitiesoftheprojectistocontinuethedevelopmentofActionSemantics,whichisthoughttobemoreunderstandabletoprogram-mersthaneitherofDenotationalSemanticsorOperationalSemantics.Italsoallowsmodularityandscalesupwell.Sofaractivitieshavemostlyconcen-tratedondescriptivepowerandonensuringunderstandabilityamongnon-specialists,butfutureactivitieswillmoveontodevelopingtheunderlyingtheory.

Amajortechniqueforprogramanalysisistheframeworkofabstractinterpretation.TheformulationandunderlyingprincipleshavebeenstronglyinfluencedbyDenotationalSemantics(atleastintheUK-Danishschool).ItisapplicabletoalllanguageshandledwellbyDenotationalSemanticsandarathergeneralframeworkforthespecificationofprogramanalyseshasbeendeveloped.Thismaythenbeusedintheimplementationofprogramminglanguageswhereonemaygeneratelessnaivecodethattakesadvantageoftheknowledgeofthe“state”suppliedbyprogramanalyses.Validatingsuchimprovedcodegenerationsispossibleinmanyinstances,butforadvancedlanguageconstructsobstaclesstillremain.AlsoitisnecessarytoincreasetheclassofprogramminglanguagestowhichthetechniquesareapplicableandmethodsbasedonOperationalSemanticsappeartobeveryfruitfulforthis.

Addingconcurrencypresentsadditionalproblemstothoseoutlinedabove.Itispossibleinprincipletovalidatethatprocessessatisfycertainspecifica-tionsbutmostsolutionsaresubjecttocombinatorialexplosion.Toimprove

3

uponthisso-calledlocaltechniqueshavebeendevelopedandanautomaticverificationtoolhasbeenconstructed.Muchresearchgoesintoextendingtheexpressivenessofspecificationswithmorequantitativeinformationlikereal-timeandpriorities.Thisisofgreatpracticalinterestandsomeprogressinthisdirectionhasbeenmade,boththeoreticallyandpracticallythroughtheconstructionofaverificationtoolforreal-timeprocesses.Amongthefuturegoalsaretheinclusionofhigher-orderandcontext-freeprocesses.Concreteapplicationshaveatendencytoproduceavastnumberofverificationgoals.MachineassistanceseemscalledforindealingwiththeseandintheprojectwehavebasedmostofourworkinthisdirectionontheHOL-system.Sofartheresultsincludethevalidationofwhileprogramsoverarbitrarytypesandtheformalisationofdomaintheory(whichisattheheartofDenotationalSemantics).ButwehavealsostudiedothertheoremprovingsystemssuchasLPinconnectionwithreasoningaboutparallelprogramsusingaTemporalLogicofActions.WeintendtocontinuesuchworkinordertoincreasetheDanishexpertiseinthispotentiallyvitalfield.Partialevaluationisanowproventechniqueforautomaticprogramtransformation.Itworksbyspecializingageneral-purposeprogramonthebasisofpartiallyknowndata.Itsmainadvantageoverotherprogramtrans-formationtechniquesisthatitisalmostcompletelyautomatic.Initialandsuccessfulapplicationsweretodevelopcompilersfrominterpreters,andau-tomaticallytoproducecompilergenerators.Significantrecentprogresshasbeenmadeinobtainingbetterexecutionefficiency,andapplicationsinotherdomainsarebeinginvestigated.Averypromisingdirectionistheautomatictransformationofspecificationsinformalisedspecificationlanguagesintoso-lutionsinprogramform.Thisworkhasalsoleadtotheoreticalinsightsintotheroleofconstantfactorsinproblemsolving,andintorelationsbetweenpartialevaluationandcomplexitytheory.Asystempartiallyevaluatingpro-gramsinthefunctionallanguageSchemehasbeendevelopedanddistributedtoseveralhundredsites.Asimilarsystembutforprogramsinthepragmat-icallyimportantimperativelanguageCisunderconstruction.

Semanticprinciplesalsoshowupinlanguagedesign.ThefunctionallanguageStandardMLhasamodulesconcept,whichisintendedformakingiteasiertowritelargeprograms.Thekeyideaisthatacertainkindofmodules,functors,canbeparameterisedonsimplermodules,structures.Wehavesucceededinextendingtheconceptoffunctor,sothatfunctorscan

4

beparameterisedonfunctorsaswellasstructures,therebyaddingtotheexpressivepowertothemoduleslanguage.RecentlytheseinsightshavebeenincorporatedwithintheMLimplementationdevelopedbyBellLabs(USA),whichisnowavailableforworld-wideuse.Relatedtothisistheuseofinferencesystemsforanalysingwhentheusualheap-basedimplementationsoffunctionallanguagesmaybereplacedbythemoreefficientstack-basedimplementationsasknownforimperativelanguages.

Ourworkalsotouchesuponotherprogrammingparadigmsincludingobjectorientedlanguages.Anumberoftechniqueshavebeendevelopedfortheanalysisofsub-classesinsuchlanguage.Asanillustrationofourbeliefthatresearchmayprogressmorerapidlywhenthetechniquesandmethodsofdifferentareasmeet,itturnedoutthatessentiallythesameclassoftechniquescouldbeusedtoimproveuponthepartialevaluationoffunctionallanguages.

2AbstractsofTalksgiven

KimGuldstrandLarsen:TimedModalSpecifications-TheoryandTools

InthistutorialwepresentthetheoryofTimedModalSpecifications(TMS)togetherwithitsimplementation,thetoolEPSILON.TMSandEPSILONaretimedextensionsofrespectivelyModalSpecificationsandtheTAVsys-tem.

ThetheoryofTMSisanextensionofreal-timedprocesscalculiwiththespecificaimofallowinglooseorpartialspecifications.Loosenessofspec-ificationsallowsimplementationdetailstobeleftout,thusallowingseveralandvaryingimplementations.Weachieveloosenessofspecificationsbyin-troducingtwomodalitiestotransitionsofspecifications:amayandamustmodality.Thisallowsustodefineanotionofrefinement,generalizinginanaturalwaytheclassicalnotionofbisimulation.Intuitively,themoremust-transitionsandthefewermay-transitionsaspecificationhas,thefineritis.Also,weintroducenotionsofrefinementsabstractingfromtimeand/orin-ternalcomputation.

TMSspecificationsmaybecombinedwithrespecttotheconstructsofthereal-timecalculusbyWangYi.The“time-sensitive”notionsofrefine-5

mentsarepreservedbytheseconstructs,thusenablingcompositionalverifica-tion.(Tobeprecise,whenabstractingfrominternalcompositionrefinement

isnotpreservedbychoicefortheusualreasons.)

EPSILONprovidesautomatictoolsforverifyingalloftherefinementspresented.WeapplyEPSILONtoacompositionalverificationofaTrainCrossingexample.

NeilJones:WhendoesSpecializationPayoffonPrac-ticalAlgorithms?

Programspecializationcanleadtosignificantrunningtimeimprovementsforanumberofwellknownandgoodalgorithmsforpracticalproblems,butnotforall;andcodeexplosionsometimesoccurs.Thetalkwilldiscussbenefitsgainedandnewproblemsencounteredinapplyingpartialevaluationtospeedupprogramsinareasoutsideprogramminglanguages.

Situationsinwhichpartialevaluationcanbeofbenefitwillbeanalyzedingeneralterms,andapplicationstocomputergraphicsandsomeotherproblemswillbedescribed.Afewtypesofprogramespeciallysusceptibletosuchoptimizationswillbecharacterized.Principlesthatleadtospeedupareemphasized,particularlyfortheubiquitous“divideandconquer”paradigm,soonecanseewhentoconsiderusingspecializationforpracticalproblems.Aclassof“oblivious”algorithmsnotsufferingfromcodeexplosionwillalsobedescribed.Surprisingly,thespeedupobtainedbyspecializingtosmallproblemsizesometimesspeedsuptheentirecomputationbynearlythesameamountasngoestoinfinity,andavoidsproblemsofcodeexplosion.

HanneRiisNielson:SemanticsasanAnalyticalTool

OneoftheproblemsstudiedintheDARTprojectis:givenaprograminalanguagewithhigher-orderabstractionmechanisms,howdoweimplementitefficientlyonarealistichardwareconfiguration.

Themaintechniquesweusearethoseofprogramanalysisandprogramtransformations.Theideaisfirsttodevelopprogramanalysesthatstaticallyextractinformationaboutthedynamicexecutionoftheprograms.Basedonthatinformationwewillnextsuggestprogramtransformationsthatwill

6

improvetheefficiencyoftheresultingimplementation.Theworkisfirmly

basedonsemanticsnotionstherebyallowingustoreasonaboutthecorrect-nessoftheprogramanalysesaswellastheprogramtransformationsinarigourousway.

InthistalkweillustratetheapproachbyshowinghowtoanalysethecommunicationbehaviourofaprograminConcurrentMLwiththeaimofimplementingitonasimpletransputerarchitecture.

KlausGrue:MathematicsandComputation

ThetalkgivesanoverviewofhowtheparallelgraphreducerdevelopedunderDARTfitsintoageneralmathematicalenvironment.Inthatenvironmentitispossibletoexpressmathematicaldefinitions,computerprogramsandmathematicalproofsinatextbookformatandtoexecutetheprogramsandverifytheproofsusingthegraphreducer.Thegoalofthisprojectistoestab-lishauniformenvironmentthatcansupporttheoreticalaswellaspracticalcomputersciencedevelopmentswithinthesamesystem.

TorbenAmtoft:Anewapproachtoconstraintbasedtypeinference

Strictnesstypes(originallyproposedbyWright)aretypeswherethefunctionarrowsareannotated:iffhastypet1→0t2weknowthatfisstrict;butiffhastypet1→1t2wedonotknowanythingforsure.Weshallpresentaninferencesystemforstrictnesstypes,formulatedintermsofconstraintsbetweenvariablesrangingover0and1.

Thecruxofourapproachistodistinguishbetweenpositiveandnegativevariables;theformer(latter)beingthoseoccurringonafunctionarrowincovariant(contravariant)position.Nowwe(roughlyspeaking)defineanor-malizedsetofconstraintstobeonewhereallconstraintsareofformb+≥s,whereb+isapositivevariableandwheresisanexpressionbuiltupfrom󰀂,󰀅andnegativevariables.

Itturnsoutthatitispossibletonormalizetheconstraintsystemontheflybyaleaftoroottraversaloftheprooftree,thatisinsteadofcollectingallconstraintsandthensolvethem.Weshallemploye.g.Tarski’sfixedpoint

7

theoreminthisprocess.

Itwouldbeinterestingtoseeifthetechniquecanbe(hasbeen?)appliedelsewhere.

KirstenLacknerSolberg:StrictnessandTotalityAnal-ysis

Forthesimplytypedlambdacalculuswithconstantsandfixedpointsandlazyevaluationwedefineastrictnessanalysis.Inthestrictnessanalysiswearelookingat,wewanttodobothstrictnessanalysisandtotalityanalysisatthesametime.Thatiswewanttodistinguishbetweentermsthataresurelybottom(doesnotevaluate;doesnothaveaWeakHeadNormalForm)andtermsthataresurelynotbottom(doesevaluate;doeshaveaWHNF).Firstwehaveanormaltypeinferenceforthelambdacalculus.Abovetheseunderlyingtypeswehavethestrictnesstypeswithstrictnessinformation.Wehavecoercionsbetweenthestrictnesstypes.Wehaveproventheanalysiscorrectwithrespecttoanaturaloperationalsemantics.

FritzHenglein&DavidSands:BindingTimeAnalysis:ModelsandLogics

Wepresentthefirstconcreteconnectionbetweenbindingtimelogics(typesystems),andthesemanticconceptofacongruentprogramdivision.Thecorrectnessoftype-basedbindingtimeanalysishasbeenarguedbyappealingdirectlytotheactionsofanofflinepartialevaluator.Bycon-trast,thecorrectnesscriterionintroducedbyJones,calledcongruence,canbearguedtobeindependentof(morefundamentalthan)thepartialevalu-ationprocess,asitisbasedonsemanticdependencieswithintheprogram,andgivesthepotentialforamoremodularapproachtothecorrectnessofabinding-time-basedpartialevaluator.

Wepresentabindingtimelogic(typesystem)whichcapturesstruc-turedbindingtimepropertiesinatypedlambdacalculuswithconstantsandrecursivelydefineddatatypes.ThesystemissoundwithrespecttothePERmodelofbindingtimes(ageneralisationofLaunchbury’sprojection-basedaccountofJones’congruencecondition)and,weconjecture,canalso

8

beshowntobecomplete(inthespiritofJensen’sstrictnesslogic)withre-specttoLaunchbury’s(finite)projectionsemantics,andHuntandSands’

PER-basedabstractinterpretation.

Theendproductofabindingtimeanalysisismorethanjustabind-ingtimepropertyfortheprogram.Itisaglobal(sticky/collecting)analysiswhichassociatesinformationwithprogrampoints.Intermsofthelogic,thisamountstoaskingnotonlywhatpropertieshold,buthow.AnexampleofsuchaglobalanalysisisLaunchbury’smonovariantbindingtimeanalysiswhichproducesacongruentprogramdivision.Itisshownthatthepro-gramdivisioniscongruentifacertainjudgmentcanbeprovedinthelogic.However,certainsimple(sound)extensionstothetypesystembreakthiscongruencecondition,suggestingthattheparticularformofLaunchbury’scongruenceconditionissomewhatoverlyrestrictive.

FlemmingNielson:FromCMLtoProcessAlgebras

Reppy’slanguageCMLextendsStandardMLofMilneretal.withprimitivesforcommunication.Itthusinheritsanotionofstrongpolymorphictypingandmaybeequippedwithastructuraloperationalsemantics.WeformulateaneffectsystemforstaticallyexpressingthecommunicationbehavioursofCMLprogramsasthesearenototherwisereflectedinthetypes.

Wethenshowhowtypesandbehavioursevolveinthecourseofcom-putation:typesmaydecreaseandbehavioursmayloosealternativesaswellasdecrease.Itwillturnoutthatthesyntaxofbehavioursisrathersimilartothatofaprocessalgebra;ourmainresultsmaythereforebeviewedasregardingthesemanticsofaprocessalgebraasanabstractionoftheseman-ticsofanunderlyingprogramminglanguage.Thisestablishesanewkindofconnectionbetween“realistic”concurrentprogramminglanguagesand“the-oretical”processalgebras.

JarlTuxenLang:ModelConstructionforImplicitSpec-ificationsinModalLogic

Intop-downdesignofreactivesystems,implicitspecificationsoftheformC(P1,...,Pn)|=Fareoftenencountered,whereC(P1,...,Pn)isasystem

9

containingthe(unknown)processesP1,...,PnandFisaspecification.WepresentamethodforconstructingtheprocessesP1,...,Pn(aslabelledtran-sitionsystems)whenCisgivenasacontextofprocessalgebra(suchasCCS),andFisgivenasaformulaofHennessy-MilnerLogicextendedwithmaximalrecursion.Themaincontributionisthetreatmentofthesimulta-neousconstructionofseveralprocesseswhichtogetheractasamodelforthespecification.Wehaveimplementedtwoprototypetools(asemi-automaticaswellasanautomaticone)whicharebasedonthepresentedtheory.JointworkwithOleHøghJensen,ChristianJeppesenandKimGuld-strandLarsen.

LarsBirkedal&MortenWelinder:PartialEvaluationofStandardML

InthistalkwedescribeofflinepartialevaluationofthecoreofStandardML,alargetypedfunctionallanguage.ItisbasedonworkforourMaster’sThe-sis.Unlikepreviouspartialevaluatorsforlargerlanguages(likeforinstanceSimilixforasubsetofSchemeorC-MixforasubsetofC)wehavechosennotdotothepartialevaluationdirectly,buttouseanuntraditionalmethodtotransformaprogramintoitsgeneratingextension.Weshowthatthisapproachisinmanyaspectssuperiortothetraditionalapproachandthatiteliminatestheneedforself-applyingthespecializer.

Wehavedevelopedabinding-timeanalysisbasedonnon-standardtypeinferenceandproduceaveryefficientimplementationofitusingconstraints.Noticethattheanalysisisimplementedandisnotonlyefficientintheorybutalsoinpractice.Whilethishasbeendonebefore,wehaveforthefirsttimesucceededinusingthetypednessofthesourcelanguagetomaketheanalysissimpleandthereforemoretrustworthy.Wedonothavetimetogointotheanalysisinthistalk.

Toourbestknowledgeourthesisalsodescribesthefirstsuccessfulstra-tegyforpartiallyevaluatingcomplicatedpatternswithvariablebindings.Earlierattemptshaveeitherbeenforamuchsimplerclassofpatternsorhavestrandedontheneed/wishforself-applicationofthespecializer.Weshowinthistalkhowthegeneratingextensionforprogramswithpatternmatchinglookslike.

10

AcompletesystemforpartialevaluationofStandardMLwithpars-ing,typechecking,binding-timeanalysis,compilergeneration,andprettyprintinghasbeenimplementedandwereportonsomeexperimentswiththissystem.Forastandardexample,compilingaprogrambyspecializinganinterpreterforasimpleflow-chartlanguage,weobtainaspeedupwhichisafactorof10biggerthanwhatotherpartialevaluatorshavegivenaccordingtotheliterature.

OlivierDanvy:OntheTransformationbetweenDirectandContinuationSemantics

Provingthecongruencebetweenadirectsemanticsandacontinuationse-manticsisoftensurprisinglycomplicatedconsideringthatdirect-stylelambda-termscanbetransformedintocontinuationstyleautomatically.However,transformingtherepresentationofadirect-stylesemanticsintocontinuationstyleusuallydoesnotyieldtheexpectedrepresentationofacontinulation-stylesemantics(i.e,onewrittenbyhand).

Thegoalofourworkistoautomatethetransformationbetweentextualrepresentationsofdirectsemanticsandofcontinuationsemantics.Essen-tially,weidentifypropertiesofadirect-stylerepresentation(e.g,totality),andwegeneralizethetransformationintocontinuationstyleaccordingly.Asaresult,wecanproducetheexpectedrepresentationofacontinuationse-mantics,automatically.

Itisimportanttounderstandthetransformationbetweenrepresenta-tionsofdirectandofcontinuationsemanticsbecauseitistheserepresen-tationsthatgetprocessedinanykindofsemantics-basedprogrammanipu-lation(e.g,compiling,compilergeneration,andpartialevaluation).Atoolproducingavarietyofcontinuation-stylerepresentationsisavaluablenewoneinaprogramming-languageworkbench.

JointworkwithJohnHatcliff,KansasStateUniversity.

Anearlierversionwaspresentedatthe9thConferenceonMathematicalFoundationsofProgrammingSemantics,NewOrleans,spring1993.

11

StenAgerholm:DomainTheoryinHOL

TheHOLsystemisaninteractiveproof-assistantsystemforconducting

proofsinhigherorderlogic.InthistalkwepresentaformalizationofdomaintheoryinHOL.Thenotionsofcompletepartialorder,continuousfunctionandinclusivepredicateareintroducedassemanticconstantsinHOLandfixedpointinductionisaderivedtheorem,justaswecanderiveothertech-niquesforrecursion.Weprovideprooftoolswhichprovecertaintermsarecpos,continuousfunctionsandinclusivepredicates,automatically.Aninter-faceandvariousdefinitiontoolsareimplementedontopofthesebasicprooftools.Inthiswayweobtainanintegratedsystemwherecpo,continuityandinclusivenessfactsareprovedbehindthescenes.

3

3.1

CurrentStatusofDART(Summer1993)

SDT:SemanticsasaDescriptiveTool(byP.D.Mosses)

TheresearchinthisareaofDARTiscentredonactionsemantics,aframe-workthatisintermediatebetweendenotationalandoperationalsemantics.Actionsemanticshassignificantpragmaticadvantagesoverotherframe-works.Forexample,itscalesupsmoothlytothedescriptionofrealisticprogramminglanguages(suchasStandardPascal),andanextensiontoadescribedlanguage(e.g.,fromStandardMLtoConcurrentML)requiresonlyanextensionofthesemanticdescription—ratherthanitswidespreadreformulation.

‘Industrial’Applications:

Thepragmaticadvantagesofactionsemanticswereacknowledgedinarecent(independent)surveyofformalsemanticstechniques.Thisledtotheadop-tionofactionsemanticsfortheformaldescriptionofANDF(Architecture-NeutralDistributionFormat,ahigh-level’universal’intermediatecodede-velopedandusedbytheOpenSoftwareFoundationandundertheESPRITprojectOMI/GLUE).TheactionsemanticdescriptionofANDFbeingde-veloped(atDDC-International)isrepresentedinRSL(theRAISESpecifi-12

cationLanguage)soastoallowtheuseofthesophisticatedtoolsavailableforRAISE.Tools:

Atoolforparsing,editing,checking,andexecutingactionsemanticde-scriptionsisunderdevelopment,incollaborationwithCWI,Amsterdam.ItisbasedonCWI’sASF+SDFsystem.Aprototypetoolwaspresentedanddemonstrated(byPDMandArievanDeursen,CWI)atAMAST’93.(TheMathematica-basedtooldevelopedearlierhasbeenshelved,soastoconcentratethemodestresourcesavailabletoSDTonthemorepromisingASF+SDF-basedtool.)LanguageDescriptions:

TheactionsemanticdescriptionofStandardPascalhasbeencompleted(byPDMandDavidWatt,Glasgow),andisavailableviaFTP.Anactionse-manticsforMLhasbeenbroughtup-to-datebyaPh.D.student(Mart´ınMusicante),andextendedtothecoreconstructsofConcurrentML.Semantics-BasedImplementation:

JensPalsberghascollaboratedwithAndersBondorfonusingtheSimilixsystemtoimplementtheactionnotationusedinactionsemanticdescriptions.AnM.Sc.student(PeterØrbæk)hasimplementedanoptimizerforactionnotation.AnotherM.Sc.student(ChristianLynbech)isinvestigatingdirectimplementationoftheformaloperationalsemanticsofactionnotation.Theory:

AnM.Sc.student(TonyJakobsen)hasdevisedandimplementedanaccuratetypeinferencealgorithmforactionnotation.Mart´ınMusicanteisinvestigat-inghowtoproveequivalencesbetweenactionsemanticdescriptionsandotherkindsofformalsemanticdescriptions.AnewPh.Dstudent(SørenB.Lassen)istodevelopthelawsandlogicofactionnotation.

13

3.2

SAT:SemanticsasanAnalyticalTool(byH.R.

Nielson)

Inthelastyearthemainactivitieshavebeenwithinthefollowingareas:ModelBasedProgramAnalysis

Wehavecontinuedourpreviousstudiesofprogramanalysisbasedonmodeltheoreticnotions,inparticularabstractinterpretation.

Thetwo-levelapproachtoprogramanalysishaspreviouslybeenusedtoverifythecorrectnessofabstractinterpretationsaswellascodegenerations.InhisM.Sc.-thesisTorbenLangeshowedhowthetechniquescanbecom-binedtoprovingthecorrectnessofanoptimizingcompiler.ThisworkwaspresentedatthePEPM’93conference.

Theefficientimplementationofabstractinterpretationreliesonthecostofcomputingfixedpoints.Apaper(byFlemmingNielson,HanneRiisNiel-son)acceptedforWSA’93presentsastructuralapproachtopredictingthenumberofunfoldingsneededtocomputethefixedpointsoffunctionalsaris-ingwhenperformingstrictnessanalysis.Anotherreport(byHanneRiisNiel-son,FlemmingNielson)suggestsvariousiterativealgorithmsforcomputingfixedpointsofspecialformsoffunctionals.LogicBasedProgramAnalysis

Recentlywehaveshiftedourattentiontowardsusinglogicalmethodsinthespecificationofprogramanalyses,inparticularwehavestudiedtheuseofannotatedtypesystems.Basicallytherearetwoapproaches:Oneistoannotatethebasetypesandtheotheristoannotatethetypeconstructors.Oneofthegoalsofthisworkistostudytheexpressivepowerofthesemethodsandtorelatethemtoexistingmodelbasedapproaches.

Theuseoflogicsystemswasalreadypioneeredinthetwo-levelapproachtoprogramanalysiswhereabindingtimeanalysiswasspecifiedusinganan-notatedtypesystem.ThisworkhasbeenrefinedbyKirstenSolberg(Odense)andanalternativetypereconstructionalgorithmbasedonconstraintsolutionhasbeendeveloped.ThisworkwaspresentedatWSA’92.

14

Strictnessanalysishasreceivedagreatdealofattentioninternationally.Wehavestudiedthespecificationofastrictnessandtotalityanalysisusinganannotatedtypesystemwithconjunctiontypesandwehaveproveditscorrectnesswithrespecttoanoperationalsemantics.Thisworkwillbereportedinaforthcomingpaper(byKirstenSolberg,FlemmingNielson,HanneRiisNielson).

Oneofthedrawbacksoftheaboveanalysisisthatitisverydifficulttoinfergoodterminationpropertiesforrecursiveprograms.Tostudythisprob-lemwehavedevelopedaterminationanalysisforalanguagewithabstractdatatypes.Thisapproachincludessomeformofwell-foundedinduction.Thecorrectnessoftheanalysisisprovedwithrespecttoanoperationalseman-ticsandshowshowwell-knownnotionsfromdenotationalsemanticssuchasmonotonicityandcontinuitycanbecapturedinanoperationalsetting.TheworkisreportedinapaperbyFlemmingNielsonandHanneRiisNielson.Finally,wehavestudiedthecorrectapplicationofstrictnessanalysisinaprogramtransformationthatintroducesthunks.Theanalysisaswellasthetransformationisspecifiedbylogicalmeansandthecorrectnessisprovedwithrespecttoanoperationalsemanticsusinganotionoflogicalrelations.ThisworkhasbeencarriedoutbyTorbenAmtoft(supportedbyDART)andwillbepresentedatWSA’93.Alsoatypereconstructionalgorithmwithconstraintsolution“onthefly”hasbeendevelopedforthestrictnessanalysis.FunctionalLanguageswithConcurrencyPrimitives

Recentlytherehasbeengreatinterestinthedevelopmentoffunctionallan-guageswithhigher-orderconcurrencyprimitives,ase.g.CMLandFacile.SeveralmembersoftheDARTprojecthaveaninterestinthisareaandaworkshopisplannedonthistopic.

Sofaronlyveryfewanalyseshavebeendevelopedfortheselanguages.Wehaveshownhowtodevelopaneffectsystemthatcapturesthecommu-nicationbehaviourofCMLprogramsandfurthermorethatthelanguageofbehaviourscanbeviewedasaprocessalgebra.Thisisanovelviewofprocessalgebrasinthatasubjectreductiontheoremfortheeffectsystemrelatestheprocessalgebratoarealisticprogramminglanguage.Thiswork(byFlem-mingNielson,HanneRiisNielson)willbepresentedatCONCUR’93.

TheaboveworkhasbeenextendedtoapolymorphicversionofCML

15

andarecentpaper(byHanneRiisNielson,FlemmingNielson)showshow

thebehaviourinformationcanbeusedtoanalysewhetherornottheCMLprogramhasafinitecommunicationtopology,i.e.whetherornotonlyafinitenumberofprocessesandchannelswillbegeneratedduringtheexecutionoftheprogram.FutureWork

Mostlikely,thefutureworkwillbecenteredaroundprogramanalysisanditsapplicationtoprogramtransformation.Weplantostudymodelbasedaswellaslogicbasedtechniquesandweshallbeinterestedinavarietyofpro-grammingparadigms,inparticularfunctionallanguageswithconcurrencyprimitives.Tobeabletohandlesuchlanguageswewillstudytheprob-lemsencounteredwhenreplacingthetraditionaldenotationalbasiswithanoperationalbasis.

ThegrouphasrecentlybeenextendedwithOlivierDanvy(AssistantProfessor)andKarolineMalmkjæer(ResearchAssistent).

3.3SOC:SemanticsofConcurrency(byK.G.Larsen)

Duringthefirsthalfof1993considerableprogresshasbeenmadewithrespecttotheanalysisof(dense)real-timesystems.Anewspecificationformalismforreal-timesystemsextendingWangYi’sTimedCalculusofCommuni-catingSystemsintoaModalTransitionSystemhasbeenintroduced.Thespecificationformalismisequippedwithanumberofequivalencesandrefin-ernentsforexpressingvarioustypesofcorrectnessproperties.AnautomatictoolEPSILONforestablishingtheseequivalencesandrefinementshasbeenconstructed.Alsoanumberof(smaller)real-timesystems(protocols,train-crossingscenarios,etc.)hasbeenanalysedusingthetool.ThisveryrecentworkhasbeenperformedincollaborationwithWangYi(UppsalaUniver-sity)andKarlisCerans(Chalmers,Gothenhurg)andwillbe(orhasbeen)presentedatanumberofconferences(MFPS’93,FME’93,CAV’93).

Ourworkoncompositionalverificationhascontinued.Inparticularanautomatictool(anditsunderlyingtheory)forsolvingsimultaneous“equa-tions”withrespecttosuitableequivalence“equations”oftheformC(X1,...,Xn)∼Shasbeenconstructed.HereX1,...,Xnaretheunknowncomponentsto

16

befound,Cisthecontextinwhichtheyareplaced,Sisthespecificationof

theoverallsystem,and∼isa“suitable”correctnessrelation.ThisworkwillbepresentedatCONCUR’93.

HenrikReifAndersen’sthesiswasexaminedthisMay.HisPhDisanimpressivepieceofwork,coveringcompositionalityandthemostefficientmodel-checkingalgorithmstodateforthemu-calculus—thiswide-rangingthesiswouldsurelymakeawelcomebook!WinskelandNielsen’shandbookchapterhasspawnedseveralresearchdevelopments:paperswithSassoneap-pearingatMFCS93andCONCUR93,andonewithJoyalatLICS93;PhDstudentsChengandTorpJensenand“speciale”(M.Sc.)studentClausenareputtingtheideastoworkinoperationalsemanticsandmodelchecking(es-peciallyofeventualityproperties)alliedwithastudyofpriority.Winskel’sbook(MITPress,January1993),inparticularitschapteronmodelcheck-ing,makesour(andtheEdinburgh-Sussex)approachestomodelcheckingaccessible.UffeEngbergisworkingonsymbolicbisimulationandtechniquesforitsdetermination,applicablealsotoprocesscalculiwithvaluepassing.ThisAugustAarhusheldahighlysuccessfultwo-weeksummerschoolon“Logicalmethodsforconcurrency”,fundedbytheHumanCapitalandMo-bilityProgramme(invitedspeakers:Dill,Harel,Moss,Stirling,Thiagarajan,Wolper).WinskellecturedattheTEMPUSsummerschoolinBrno.Finally,theoreticalworkoncalculimixingthefunctionalandparallelparadigmhasbeencarriedout.Inparticular,anextensiveanalysisofequiv-alencesandtheiraxiomatizationwithintheForkcalculus(a“projection”ofCML)hasbeenoffered,andhasbeenpresentedatICALP’93.Preliminaryworkondynamictypingofsuchmixedcalculihasbeenstudied,andwillbesubjectforfuturework.Thishasmanypointsofcontactwiththeworkon“FunctionalLanguageswithConcurrencyPrimitives”pursuedunder“Se-manticsasanAnalyticalTool”.

3.4SBD:SemanticsBasedDeduction(byG.Winskel)

APhDstudent(UrbanEngberg)continueshisimplementationofasystemtosupportproofsinTLA,thetermporallogicofLamportwithwhomheisinclosecorrespondence.Thisworkoverlapswiththearea“SemanticsofConcurrency”.

17

StenAgerholm(fundedbyDART)hasbeensuccessfulinimplementingasignificantpartofdomaintheoryintheproofassistantHOL.TheadvantageofHOLoverLCFisthatthemetalanguageofHOLallowsmuchmoregeneralreasoning,sometimesnecessaryinarguingaboutinclusivepredicatesorusingthenewcoinductionprinciplesforrecursivedatatypes.Thisworkhasledtoapaper,tobepresentedattheInternationalHOLmeetinginVancouver,andtoappearintheproceedings.

AgerholmandWinskelhavejointlysupervisedHougaard’sstudentprojectoncomputability,recentlycompletedandreceivinggrade13.Agerholmwillgivea3weekcourseinHOLaspartofMosses’graduatecourseinLogicintheFall.ThismayinvolveothersfromTFL,withwhomAgerholmhasbegunatentativecollaborationonextendingHOLtools.

Theoreticalworkcontinuesinseveralareas.Inparticular,UffeEngbergandWinskel’scompletenessresultsforlinearlogicwithrespecttoPetrinetsasamodelaretoappearinMFCS93.LinearlogicreappearsinthePhDworkofBrauner,SørensenandCattani.Inparticular,Sørensen’sworkusingideasfromcategorytheorytoincludetimeindomainswasboostedbyWinskel’smeetingwithP-LCurien—thelatterhasasemanticsforlinearlogicincon-cretedomains.Linearlogic,andespeciallylinearclassicallogic,areleadingtoarefinedanalysisofdomainssuitablefordenotationalsemantics,andaresheddinglightoftheoldandhardPCFfullabstractionproblem.

3.5

SBPM:SemanticsBasedProgramManipulation(byN.D.Jones)

Overview

ThispartofDARTisstillverymuchontrackwithsignificantoutsiderecogni-tion,andmanyinterestingtaskstobedoneandleadstobefollowed.Increas-ingcollaborationwithinDARTisevidencedbyjointworkbetweenBondorfandPalsberg,twoAarhusPh.D.degreesinSBPM(AmtoftandPalsberg,withcensorfromDIKU),andbyemploymentatDAIMIofpartialevalua-tionresearchersO.DanvyandK.Malmkjær(earlieratDIKU).

TherehasbeenmuchresearchandeducationalactivityinthisareasinceSeptember1992withnumerouspublishedarticles,someinjournalsandsomeinavarietyofhigh-levelconferencesincludingIFIPW.G.2.8Functional

18

Programming,FormalMethodsinProgrammingandApplications,FPGA,PARLE,PEPM,PLILP,StateinProgrammingLanguages,STOC,andtheWorkshoponStaticAnalysis.InadditionaspecialissueoftheJournalofFunctionalProgrammingwasguesteditedbyNeilJones.AnewbookcollectingmanyresultsaccomplishedunderDARTwaspublished:PartialEvaluationandAutomaticProgramGenerationbyJones,Gomard,Sestoft(PrenticeHallInternational,425pp.).

Education.AD.Sc.thesiswasdefendedatDIKUbyKlausGrue(withHenkBarendregtascensor),and5studentsareworkingonPh.D.degrees:LarsOleAndersen,JesperJørgensen,ChristianMossin,KristofferRose,andMortenWelinder.3M.Sc.theseswerewritten,byChristianMossin,EigillRosager,andonejointlybyLarsBirkedalandMortenWelinder.

Guests.Wehaveunusuallymanyguestsin1993-1994—allofwhomcamewithfundingfromoutsideDenmark,andfor1yearormore:

Assoc.Prof.RobertPaige(NewYorkUniversityCourantInstitute),ThomasRepsandSusanHorwitz(UniversityofWisconsin),Assis.Prof.RobertGl¨uck(TechnicalUniversityofVienna),ResearchersRyoNakashige(HitachiJapan)andShmuelSagiv(IBMIsrael),graduatestudentLiPingZong(AcademiaSinica,Beijing).

Staff.LarsBirkedalwasappointedasresearchassistantunderDARTfunds,andJakobRehofintheDARTareabyaguest’sfunds.DavidSands(ImperialCollege,London)wasemployedaspostdoctoralguestduringallof1993.MuchusefulworkhasbeendonebyDART-employedprogrammerPeterHolstAndersen.

1993internationalmeetingsheldatDIKU.IFIPWorkingGroup2.8onFunctionalProgramming(40participants),FPCA:FunctionalPro-grammingandComputerArchitecture(180participants),SIPL:StateinProgrammingLanguages(80participants),PEPM:PartialEvaluationandSemantics-BasedProgramManipulation(80participants).Researchgoalsandtheirevolution

Thispastyearhasseenthefirstpracticalapplicationofanewtechniqueforpartialevaluation:constructionofhand-writtenversionsof“cogen”,ratherthanproducing“cogen”byself-applying“mix”.Thishasseveraladvantages,

19

particularlyforstronglytypedlanguagesandforpatternmatching,andhasbeenusedinallthethreesystemsdescribedbelow.

FurtherdevelopmentofSimilix.Version5ofthismatureandmuch-copiedpartialevaluatorforSchemewasrecentlyreleased.Itisnowmoreuser-friendlyandsignificantlymoreefficient,bothinthecodeitgeneratesandinitstransformationspeed.GroupsoutsideDenmarkarepublishingpapersusingSimilix.

DevelopmentofC-mix.AnM.Sc.thesisdescribingthissystembyL.O.Andersenwasawardedaprizein1992,andhasbeendevelopedconsid-erablysincethen.Ithasbeenextendedandappliedtovariousproblems,arecentapplicationbeingan“off-the-shelf”raytracingprogramselectedfromatextbookonComputerGraphics.C-mix,byspecializingthetracertoafixedscene,resultedinaprogramthatranaroundtwiceasfastastheorigi-nal.InthisuseofC-mix,arelativelysmallamountoftuningwassufficienttoobtaintheobservedspeedup.

Theexperimentisconvincingsincethe“off-the-shelf”programhadbeenengineeredtobeespeciallyfast.Currentworkconcernsstrengtheningthesystem,andmakingitmoreuser-friendly,robust,andefficient.

DevelopmentofML-mix.AthesisbyL.BirkedalandM.WelinderonapartialevaluatorforMLwasawardedthehighestpossiblegrade.MLisamuchlarger,morecomplex,andwidelyusedlanguagethanSimilix’slanguageSCHEME.This(rathersophisticated)MLpartialevaluatorbuildstoahighdegreeonexperiencesgatheredfromtworesearchenviromnents:thoseofSimilixandofML.

ML-mixisquitenew,butpeopleintheUSandEnglandhavealreadyshowninterestinusingit(BellLabs,andTomMelhamfortheHOLappli-cationmentionedbelow).Muchremainstobedonebutthecoreisrobustandwell-founded,soML-mixpreservesexactlyitsinputprogram’ssemanticsduringtransformation(essentialfortoolstobeusedbyothers).Itshouldclearlybedevelopedfurther.

Staticprogramanalyses.Severalnewprogramanalysesweredevel-opedandimplemented,includingthoseusedinSimilix,C-mix,andML-mix.

20

Futureplans

Wewillcontinuetopursueourcurrentresearchdirections,andaswellto

lookintothefollowingleads,whichindicateanincreasingoutsideinterestinpartialevaluation.

TheHOLsystem.(HigherOrderLogic)isatheoreticallybasedsys-temwithwidespreadpracticalandindustrialuse;butasystemwhoseruntimeisoftenalimitingfactor.ItiscurrentlyusedbyDARTmembersAarhusandAalborg.AcentralHOLfigure,TomMelham(CambridgeandGlasgow),recentlylecturedonthepossibilityofusingML-mixtospeedthesystemup,andwillvisitDIKUthisFalltoinvestigateitsfeasibility.Thiscouldbeasignificantapplicationofpartialevaluation,duetoHOL’swidespreaduse.ERSEMisanEC-supportedprojectforcomputationalecologicalmo-delingoftheNorthSea,withsixEuropeanpartners.Theirnewsimulationpackage,writteninC,hassignificantcomputationalbottlenecks.Handa-nalysisindicatesthatpartialevaluationcouldmakemanyoftheirprogramsrunatleasttwiceasfast.ERSEMplansapilotstudywithDIKUofpartialevaluationautomaticallytoimprovetheirprograms.Thisisinteresting,asitteststhescalabilityofourmethodstorealisticproblemsnotdevisedbyourselves.

3.6

OST:OperationalSemantics,TypesandLanguageImplementation(byM.Tofte)

Theprojectproposaldefinedthreeareasofactivities:thesemanticsofhigher-orderfunctorsinML,typeinferenceandstorageallocation,andtheMLKit.Progressintheseareashasbeenasfollows:Higher-orderFunctors

Wehaveexploredthesemanticsoffunctorapplicationinthepresenseofhigher-orderfunctors.Anewstyleofinferencerulesfordefiningtheseman-ticsofmodulesisunderdevelopment.Thepurposeistosimplifyearlierapproachestomodulessemanticsandtobeabletodefinetheoperationsofstructurematchingandpropagationofsharinginamoreoperationalway,byencodingtheminatypedλ-calculuswithdependenciesatthetypelevel

21

formalizedbyanabstractionmechanism.ThisworkisjointworkwithDavidB.MacQueen,fromA.T.&T.BellLabsinNewJersey.TypeInferenceandStorageAllocation

Wehavegeneralizedtyperegioninferencesystemtohandlepolymorphicre-cursioninregions.Thismeansthatdifferentinvocationsofthesamefunctioncanoperateondifferentregions.Formanyfunctions,theeffectofregionin-ferenceistore-discoverregionsthatcorrespondtotheusualstackframesinanormalstack-basedimplementationofblock-structuredlanguages.(How-ever,unlikenormalstackimplementations,regioninferenceisalsoabletohandlehigher-orderfunctionsandrecursivedatatypes.)Wehavedevelopedseveralregioninferencealgorithmsandimplementedoneofthem.Further-more,wehavemeasuredthespacerequirementsofsampleprograms,whentheyarecompiledbytheregioninferencealgorithmandinterpretedonanab-stractmachine.Theresultsshowthatinmostcases,spacerequirementsareverymodestindeed.Theyalsoshowthatregionallocationanddeallocationisextremelyfrequentandmustbemadeveryefficientlyinarealimplementa-tion.Wearecurrentlylookingatwaysofachievingthis.Also,wearewritingacompilerfromregion-annotatedprogramstoCandaruntimesysteminC.ThissoftwarewillbeintegratedwiththeMLKit.Whencompleted,thissystemwillallowustoobtainfiguresforactualrunningtimes.

ThisworkhasbeendonebyMadsTofteandLarsBirkedalincollabo-rationwithJean-PierreTalpin,EcoledesMines,Paris.TheMLKit

Version1oftheMLKithasbeencompletedandmadeavailableviaanony-mousftp.About45sitescopiedit.ThedocumentationoftheMLKithasbeenmadeintoatechnicalreportatDIKU.

StudentsatDIKUhavebeenusingtheMLKitforvariousprojects,forinstancePeterSkadhaugehasimplementedatypecheckerbasedonsemi-unification,byreplacingsomeofthemodulesoftheMLKitbymodulesforgeneratingandsolvingsystemsofequationsandinequalities.

22

3.7

3.7.1

OtherTopics

Types,Constraints,andAnalysis(byM.Schwartzbach)

Thisyearhasseentheroundingoffofseveralprojects,aswellastheinitiation

ofnewactivities.

ThejointworkwithJensPalsbergonstaticanalysisofobject-orientedlanguageshasbeenmaturedthroughcooperationwithOleAgesenofStan-fordUniversity.Ourconstraint-basedalgorithmshavebeenextendedandrefinedtoproduceafull-scaleimplementationfortheSELFlanguagebeingdevelopedbySUNMicrosystems.WhileSELFisgenerallyrecognizedasamostchallenginglanguage,ourstaticanalysesnowformthebasisforseveraltoolsthatarebeingintegratedintothestandardprogrammingenvironment.JensPalsbergandMichaelSchwartzbachhaveforsometimenowworkedonobject-orientedtypesystems.Thisactivityisbeingsummedupinourrecentbook,whichwillbepublishedbyWileyinSeptember1993.Accom-panyingthisadvancedundergraduatetext,aforthcomingjournalarticlewillcontainthesemanticalfoundationsforourapproach.

TheworkwithNilsKlarlundongraphtypeshasbeencontinued.Guidedbytheprinciplethatdatatypesareinvariants,wedevisealogicalandde-cidableframeworkforexpressingglobalpropertiesofastoreconsistingofrecordsandpointers.Commonproperties,whichseemtohavecalledforafullHoarelogicbeyondthereachoftypecheckinganddecidability,cannowbeexpressedinauniformdescriptivelanguageintegratingtypesandprogramassertions.Ourcontributionsare:aformalismfordescribingstoresbasedonmonadicsecond-orderlogicandourconceptofpointerconstraint;anextensionofthemethodofsemanticinterpretationtoshowdecidabilityofHoaretriples;andasketchofanovelsoftwaremethodologysuggestedbytheextensiveautomatedanalysisthatfollowsfromourtechniques.Arecentproject,jointwithJensPalsbergandBjornFreeman-Benson,aimstoperformstaticanalysisofconstraintimperativeprograms,inordertoconservativelyapproximatefreenessofvariablesandsatisfiabilityofcon-straints.

23

3.7.2MapTheoryandParallelGraphReduction(byK.Grue)

Concerningmaptheory,DARThasfundedpartofatraveltoParistovisitUniversityVII.Heremaptheorywaspresentedanddiscussed,andanoutlineofasimplifiedconsistencyproofwasestablished.AjointpaperwithChantalBerlineonthesimplifiedproofisunderpreparation.

LarsLassenhasdefinedafunctionallanguageandimplementedacom-pilerwhichallowstoexecuteprogramsontheparallelgraphreducer.ThelanguageisveryclosetoasubsetofCommonLisp.MartinFunkLarsenhasimplementedanumberofalgorithmsinthatsubsetofCommonLispandisnowreadytorunthemontheparallelgraphreducer.Thisallowsbenchmarkingofthegraphreduceronmediumsizesoftware.3.7.3

ActivitiesatTheTechnicalUniversity(byB.S.Hansen)

PeterSestoftisstudyingvaliditycheckingforasubsetofDurationCalculus.Oneoftheresultsisanimplementation.Theproblemturnedouttohaveveryhighcomplexity,soalternativeapproachesarebeingconsidered(jointworkwithM.R.Hansen,J.U.Skakkebæk,ZhouChaochen).

AcurrentstudentprojectsupervisedbyPeterSestoftconcernsnon-self-applicablepartialevaluationofasubsetofStandardML.

BoStigHansenisworkingjointlywithFlemmingM.Dammontypesystemsincludingasettheoreticunionoperator.Thishasresultedinde-cidabilityresultsforthesubtyperelationinasystemwithunion,product,functionspaceandrecursion.ApaperontypecheckingbygenerationofproofobligationshasbeenacceptedfortheWorkshoponSemanticsofSpec-ificationLanguages,October1993;theproofobligationsensureabsenceofrun-timetypeerrors.

4ExternalandInternalCooperation

Membersoftheprojectparticipateinanumberofinternationalresearchprojects.AlsomembersinAarhusandAalborgparticipateinthenewlycreatedBRICSproject,acentreforBasicResearchinComputerScience,fundedbyTheDanishResearchFoundation.Alsowhentheneedarises

24

smallerworkshopsarearrangedonspecifictopics.

4.1ParticipationinInternationalProjects

CONCUR2

Concurrencytheoryisimportantforthespecificationandverificationofcon-currentanddistributedsystems.CONCUR2isanEspritBasicResearch

Actionwiththespecificaimatextendingprocessalgebraandlogicalcalculitoincorporatereal-timeaspects,probabilisticnon-determinism,valuepass-ingandinfinitestatespaces.CONCUR2aimsforaunifiedviewonprocessalgebra,andintendstodesign,specifyandimplementsupportingsoftwaretools,andcommonformatsandinterfacesforsuchtools.

PartnersofCONCUR2besidesAalborgUniversityare:CWI,Edin-burgh,Eindhoven,INRIASophiaAntipolis,Oxford,SussexandSICS.CLICS

Winskel’sEspritBRA“CategoricalLogicinComputerScience”fundsthecategorytheoristandprooftheoristSergeiSoloviev(onleavefromtheUni-versityofSt.Petersburg)andwill,inaddition,employClaudioHermidathisFall.Semantique

SemantiqueisanEspritworkinggrouponSemantics-BasedProgramMa-nipulation.IthasaspartnersChalmersUniversity(Gothenburg),Univer-´sityofAarhus,UniversityofCopenhagen,EcoleNormaleSup´erieure(Paris),

ImperialCollegeofScience,TechnologyandMedicine(London),andtheUniversityofGlasgow.ImperialCollegeisthecoordinator.Atlantique

AtlantiqueisanewEspritworkinggroupwhosepurposeistofacilitateEuropean-Americanjointresearchinthesamearea.ItconsistsoftheEuro-peansabove,pluseightAmericanresearchgroups:CarnegieMellonUniver-25

sity,theCityUniversityofNewYork,KansasStateUniversity,NortheasternUniversity,NewYorkUniversity:CourantInstitute,OregonGraduateInsti-tute,StanfordUniversity,andYaleUniversity.DIKUisthecoordinatorofAtlantique.

TheEspritgranttoAtlantiqueincludestravelbyresearchersandstu-dentsamongtheEuropeanpartnersforresearchcooperationforshorterpe-riodsofrescarchcooperation(afewdaystoafewweeks).Further,weun-derstandthatNSF,theAmericanNationalScienceFoundation,willfundstudentvisitsfromtheUStotheEuropeanpartners.COMPASS

PeterMossesisamemberofESPRITBasicResearchWorkingGroup6112COMPASS:AComprehensiveAlgebraicApproachtoSystemSpecificationandDevelopment.Thepartnersofthisworkinggrouparethe19majorEuropeansitesforresearchonalgebraicspecification,locatedatuniversitiesandresearchinstitutesinAarhus,Barcelona,Berlin,Braunschweig,Dresden,Edinburgh,Genoa,Lisbon,Munich,Nancy,Nijmegen,Oslo,Oxford,Paris,andSaarbr¨ucken.ML2000

MadsTofteisamemberoftheML2000group.Thisgroupisdesigninganewprogramminglanguage(ML2000),whichisintendedtobeasuccessortoStandardMLbytheyear2000.ThegroupconsistsofAndrewAppel(Prince-tonUniversity),LucaCardelli(DECSRC),CarlGunter(UniversityofPenn-sylvania),ElsaGunter(AT&TBellLabs),RobertHarper(CarnegieMellonUniversity),DavidMacQueen(AT&TBellLabs),JohnMitchell(StanfordUniversity),JohnRiecke(AT&TBellLabs),JohnReppy(AT&TBellLabs),MadsTofte(DIKU)andXavierLeroy(StanfordUniversity).ProCoSII

TheworkbyPeterSestoftonvaliditycheckingforasubsetofDurationCal-culushasbeendoneinclosecollaborationwiththeESPRITprojectProCoSII.

26

LOMAPS

LOMAPSisanacronymforLogicalandOperationalMethodsintheAnalysis

ofProgramsandSystems.ItisanESPRITBRAproject(startingfall1993)onthedevelopmentofadvancedmethodsforanalysingandverifyingproper-tiesofmultiparadigmaticprogramminglanguageslikefunctionallanguageswithconcurrencyprimitives.Thesemanticframeworkwillbeoperationalsemanticsandforthespecificationofanalysesvariouslogicalapproacheswillbeexplored.

Thefollowingsitesparticipateintheproject:AarhusUniversity(coor-dinator),SwedishInstituteofComputerScience,EcoledesMines,EuropeanComputer-IndustryResearchCentre,CambridgeUniversity,UniversityofPisa,EcoleNormaleSuperieureandEcolePolytechnique.

4.2

Mini-workshoponProgramAnalysis(byH.R.Niel-son)

OnOctober2ndasmallworkshopdevotedtoprogramanalysiswasheldatDAIMI.ThepurposewastohaveasettingforpresentinganddiscussingcurrentworkwithtwoguestsatDAIMI:OlivierDanvy,KansasStateUni-versity,USAandKarolineMalmkjær,KansasStateUniversity,USA.Themeetingwascenteredaroundfourtalks:

KarolineMalmkjær,DepartmentofInformationandComputerSciences,KansasStateUniversity:Predictingpropertiesofresid-ualprograms

Wepresentananalysisdetectingstructuralpropertiesoftheresultsofpar-tialevaluatorsforScheme-likelanguages.Theanalysisisbasedonabstractinterpretationofthegeneratingextensionproducedbythepartialevaluator.Ithasrecentlybeenextendedtohandlehigher-orderfunctions.JensPalsberg,DAIMI:CorrectnessofbindingtimeanalysisAbindingtimeanalysisiscorrectifitalwaysproducesconsistentbindingtimeinformation.Consistencymeansthatifthebindingtimeinformationis

27

usedbyapartialevaluatorthenthepartialevaluatorcannotcommiterrorssuchasapplyingsomethingunknowntoanargument.Asufficientanddecid-ableconditionforconsistency,calledwell-annotatedness,wasfirstpresentedbyGomardandJones.

Inthistalkwepresentaweakerconsistencycondition.Ourconditionisdecidable,subsumestheoneofGomardandJones,andwasfirststudiedbySchwartzbachandthespeaker.

Wehaveprovedthatourconditionindeedimpliesconsistency.Asacorollary,wegetthefirstproofofcorrectnessofthecoreofthebindingtimeanalysesofBondorf,ConselandMogensen.Wehavealsoprovedthatawholefamilyofpartialevaluatorswillonterminationhaveeliminatedall“eliminable”-markedpartsofaninputwhichsatisfiesourcondition.ThisgeneralizesaresultofGomard.Ourdevelopmentisforthepureλ-calculuswithexplicitbindingtimeannotations.

OlivierDanvy,DepartmentofInformationandComputerSciences,KansasStateUniversity:Oncontinuation-passingstyle

Continuation-passingstyle(CPS)isaprogrammingstylestressingthecon-trolflowofaprogramandallowingtoexpressfunctionallyoperationsthatarenon-functionalapriori(jumps,exceptions,coroutines,etc.)Itsessentialproperty:aCPSprogramyieldsthesameresultindependentlyofitsevalua-tionstrategy—callbynameorcallbyvalue.Itsdomainofapplicationvarysurprisingly:proofofalgorithmtermination,semantics-directedcompiling,compilergeneration,parallelization,single-threadingdetection,doublenega-tioneliminationinprooftheory,andsoon.ThisvarietyisreflectedbyanumberofspecificationsoftheCPStransformation—instrikingcontrastwiththe3-lines&2-passes(transformation+simplification)oftheoriginalliterature[Fischer,Reynolds,Plotkin].

ThegoalofthistalkistoenlightenCPSbygoingbacktothesources,i.e.totheoriginal3-linesand2-passesspecification.Byasimpletransformationofthisspecification,weobtainastaticseparationoftheresultsintermsof“essential”and“administrative”constructs(verymuchlikeBindingTimeAnalysis).Byinterpretingtheessentialconstructionsassyntaxconstructorsandadministrativeconstructionsasexecutablecode,weobtainaone-passtransformationalgorithm.

28

Wealsoconsideredtheinversetransformation:theDirectStyletrans-formation.ThistransformationanditsproofsuggesttoreformulatetheCPStransformationin3successivepassesthatappearconsiderablysimplerthanthe2originalpasses.

Finally,wesituatethisdevelopmentamongrelatedwork.PartofthisworkisjointworkwithAndrzejFilinski.

TorbenLange,DAIMI:Thecorrectnessofanoptimizedcodegen-eration

Foralazyfunctionalprogramminglanguagewithcombinators,wefirstspec-ifyastandardsemanticsandastrictnessanalysisuponthelanguage.Usingtheinformationfromtheanalysiswecanspecifyanoptimizedcodegenera-tionavoidingdelayclosuresotherwisegeneratedaroundtheargumenttoanapplication.Bydefiningalayerofadmissiblepredicateswearefinallyabletoprovethecorrectnessofthecodegenerationwithrespecttothestandardsemantics.

5

PublicationsfromDART(fromMarch1991toAugust1993)

Belowwelistthepublicationsfromtheproject.TheoverallcriterionhasbeenthatpublicationtookplaceintheperiodfromMarch1991toAugust1993,butwehavemarkedwithanasteriskthoseentrieswherealmostallscientificworkwasperformedbeforeMarch1991.

References

[Aceto1]L.AcetoandU.H.Engberg,

“Failuressemanticsforasimpleprocesslangnagewithrefinement,”inFSTandTCS11,vol.560ofLectureNotesinComputerScience,pp.89-108,Springer-Verlag,1991.[DAR.T-129].

29

[Aceto2]L.AcetoandA.Ing´olfsd´ottir,

“AtheoryoftestingforACP,”

inProceedingsofCONCUR’91,LectureNotesinComputerScience,1991.[DART-l].[Agerholm1]S.Agerholm,

“MechanizingprogramverificationinHOL,”

inProceedingsoftheInternationalHOLusersMeeting,Davis,Califor-nia,1991.[DART-2].[Agerholm2]S.Agerholm,

“MechanizingprogramverificationinHOL,”

Tech.Rep.DAIMIIR-111,ComputerScienceDept.,AarhusUniv.,1992.[DART-197].[Agerholm3]S.Agerholm,

“DomaintheoryinHOL,”

inProceedingsofthe1993InternationalMeetingonHigherOrderLogicTheoremProvingandItsApplications,VancouverCanada,11-13Au-gust1993,

LectureNotesinComputerScience,Springer-Verlag,1993.[DART-198].[Amtoft1]T.Amtoft,

“Propertiesofunfolding-basedmeta-levelsystems,”

inProceedingsoftheSymposiumonPartialEvaluationandSemantics-BasedProgramManipulation,

SIGPLANNOTICESvol.26,no.9,pp.243-254,1991.[DART-3].[Amtoft2]T.Amtoft,

“Unfold/foldtransformationspreservingterminationproperties,”

in4thInternationalSymposiumonProgrammingLanguageImplemen-tationandLogicProgramming(PLILP92),Leuven,Belgium(M.BruynoogheandM.Wirsing,eds.),vol.631ofLectureNotesinCom-puterScience,pp.187-201,Springer-Verlag,1992.[DART-133].[Amtoft3]T.Amtoft,

“Minimalthunkification,”

in3rdInternationalWorkshoponStaticAnalysis(WSA’93),September1993,Padova,Italy,no.724inLectureNotesinComputerScience,pp.218-229,Springer-Verlag,1993.[DART-168].

30

[Amtoft3]T.Amtoft,

SharingofComputations.

PhDthesis,ComputerScienceDept.,AarhusUniv.,1993.DAIMI-technicalreportPB-453.[DART-169].[Amtoft4]T.Amtoft,

“Strictnesstypes:Aninferencealgorithmandanapplication,”

TechnicalMonographDAIMIPB-448,ComputerScienceDept.,AarhusUniv.,1993.[DART-167].[Amtoft5]T.AmtoftandJ.LarssonTr¨aff,

“Partialmemorizationforobtaininglineartimebehaviorofa2DPDA,”TheoreticalComputerScience,vol.98,pp.347-356,1992.[DART-4].[Andersen1]H.R.Andersen,

“Localcomputationofalternatingfixed-points,”

Tech.Rep.260,ComputerLaboratory,UniversityofCambridge,1992.[DART-5].[Andersen2]H.R.Andersen,

“Localcomputationofsimultaneousfixed-points,”

TechnicalMonographDAIMIPB-420,ComputerScienceDept.,AarhusUniv.,1992.Submittedforpublication.[DART-6].[Andersen3]H.R.Andersen,

“Modelcheckingandbooleangraphs,”

inProceedingsofESOP’92,vol.582ofLectureNotesinComputerSci-ence,Springer-Verlag,1992.[DART-7].[AndersenWinskel1]H.R.AndersenandG.Winskel,

“Compositionalcheckingofsatisfaction,”

inProceedingsofCAV,Aalborg,vol.575ofLectureNotesinComputerScience,Springer-Verlag,1991.Extendedabstract.JournalversionasDART-9.[DART-8].[AndersenWinskel2]H.R.AndersenandG.Winskel,

“Compositionalcheckingofsatisfaction,”

FormalMethodsinSystemDesign,vol.1,1992.ExtendedabstractasDART-8.[DART-9].

31

[LAndersen]L.Andersen,

“Binding-timeanalysisandthetamingofCpointers,”

inProc.ofACMSymposiumonPartialEvaluationandSemantics-BasedProgramManipulation,PEPM’93(D.Schmidt,ed.),1993.Toappear.[DART-146].[LOAndersen1]L.O.Andersen,

“Cprogramspecialization,”

Tech.Rep.12/14,DIKU,UniversityofCopenhagen,Denmark,Uni-versitetsparken1,DK-2100CopenhagenEast,1992.(revisedversion).[DART-12].[LOAndersen2]L.O.Andersen,

“PartialevaluationofCandautomaticcompilergeneration(extendedabstract),”

inProceedingsofCompilerConstructions-4thInternationalConfer-ence,CC’92(U.KastensandP.Pfahler,eds.),vol.641ofLectureNotesinComputerScience,pp.251-257,Springer-Verlag,1992.[DART-13].[LOAndersen3]L.O.Andersen,

“Self-applicableCprogramspecialization,”

inProceedingofPEPM’92:PartialEvaluationandSemantics-BasedProgramManipulation,pp.54-61,1992.AvailableasTechnicalReportfromYaleUniversity.[DART-10].[LOAndersenGomard]L.O.AndersenandC.K.Gomard,

“Speedupanalysisinpartialevaluation:Preliminaryresults,”

inProc.ofWorkshoponPartialEvaluationandSemantics-BasedPro-gramManipulation(PEPM’92),pp.1-7,1992.AvailableasTechnicalReportfromYaleUniversity.[DART-11].[PHAndersen]P.H.Andersen,

“Partialevaluationappliedtoraytracing.”Unpublished,1993.[DART-l91].

[BirkedalRothwellTofteTurner]L.Birkedal,N.Rothwell,M.Tofte,andD.

N.Turner,

“TheMLkit(version1),”

32

Tech.Rep.DIKU-report93/14,DepartmentofComputerScience,Uni-versityofCopenhagen,Universitetsparken1,DK-2100Copenhagen,1993.[DART-194].

[BirkedalWelinder]L.BirkedalandM.Welinder,

“PartialevaluationofStandardML,”

Master’sthesis,DIKU,UniversityofCopenhagen,Denmark,1993.[DART-189].[Bondorf1]A.Bondorf,

“Compilinglazinessbypartialevaluation,”

inFunctionalProgramming,Glasgow1990.WorkshopsinComputing(S.L.P.Jones,G.Hutton,andC.K.Holst,eds.),pp.9-22,Springer-Verlag,1991.[DART-14].∗[Bondorf2]A.Bondorf,

“Similixmanual,systemversion3.0,”

Tech.Rep.91/9,DIKU,UniversityofCopenhagen,Denmark,1991.[DART-15].[Bondorf3]A.Bondorf,

“Similixmanual,systemversion4.0.”

IncludedinSimilixdistribution,1991.[DART-16].

[Bondorf4]A.Bondorf,

“ImprovingbindingtimeswithoutexplicitCPS-conversion,”

in1992ACMConferenceonLispandFunctionalProgramming.SanFrancisco,California,pp.1-10,1992.[DART-17].[Bondorf5]A.Bondorf,

Similix5.0Manual.

DIKU,UniversityofCopenhagen,Denmark,1993.IncludedinSimilixdistribution,82pages.[DART-174].[BondorfJorgensen1]A.BondorfandJ.Jørgensen,

“Efficientanalysesforrealisticoff-linepartialevaluation,”

JournalofFunctionalProgramming,specialissueonpartialevaluation,vol.11,1993.[DART-175].[BondorfJorgensen2]A.BondorfandJ.Jørgensen,

“Efficientanalysesforrealisticoff-linepartialevaluation,”

33

Tech.Rep.93/4,DIKU,UniversityofCopenhagen,Denmark,1993.[DART-145l.

[BondorfPalsberg]A.BondorfandJ.Palsberg,

“Compilingactionsbypartialevaluation,”

inFPCA’93,ConferenceonFunctionalProgrammingandComputerAr-chitecture,Copenhagen,Denmark,pp.308-317,ACM,1993.[DART-176].[Borjesson]A.Børjesson,

“DistinguishingpropertiesandmodelcheckinginTAV.”Inpreparation,1992.[DART-18].[BorjessonLarsen]A.BørjessonandK.G.Larsen,

“EquationsolvingusingTAV.”Inpreparation,1992.[DART-19].

[BorjessonLarsenSkou]A.Børjesson,K.G.Larsen,andA.Skou,

“GeneralityindesignandcompositionalverificationusingTAV,”InProceedingsofFORTE’92,1992.Toappear.[DART-20].[CamilleriWinskel]J.A.CamilleriandG.Winskel,

“CCSwithprioritychoice,”

InProceedingsofLICS’91,1991.ToappearinInformationandCompu-tation.[DART-21].[Cerans]K.Cerans,

“Decidabilityofbisimulationequivalencesforparalleltimerprocesses,”inProceedingsofCAV’92,LectureNotesinComputerScience,1992.[DART-22].[CeransGodskesenLarsen]K.Cerans,J.Godskesen,andK.Larsen,

“Timedmodalspecifications-theoryandtools,”

tech.rep.,AalborgUniversity,Dept.ofMath.andComp.Sc.,1993.[DART-154].[ChristensenHuttelStirling]S.Christensen,H.Huttel,andC.Stirling,

“Bisimulationequivalenceisdecidableforallcontext-freeprocesses,”inProceedingsofCONCUR’92,vol.630oflectureNotesinComputerScience,Springer-Verlag,1992.ECS-LFCS-92.[DART-23].

34

[Dybkjaer]H.Dybkjær,

CategoryTheory,Types,andProgrammingLanguages.

PhDthesis,DIKU,UniversityofCopenhagen,Denmark,1991.vi+146pp.AvailableasDIKUreport91/11.[DART-24].∗[DybkjaerMelton]H.DybkjærandA.Melton,

“ComparingHagino’scategoricalprogramminglanguageandtypedlambdacalculi,”

TheoreticalComputerScience,vol.111,pp.145-189,1993.[DART-25].∗[EngbergGronningLamport]U.Engberg,P.Grønning,andL.Lamport,

“MechanicalverificationofconcurrentsystemswithTLA.”

ToappearintheProceedingsoftheFourthInternationalWorkshoponComputer-AidedVerification,1992.[DART-26].[EngbergWinskel]U.H.EngbergandG.Winskel,

“CompletenessresultsforlinearlogiconPetriNets.”SubmittedtoMFCS’93,Gda´nsk,Poland,August30-September3,1993.

FullversionwillappearasDAIMIPB,1993.[DART-153].[Gammelgaard1]A.Gammelgaard,

“Constructingsimulationschunkbychunk,”

InternalReportDAIMIIR106,ComputerScienceDept.,AarhusUniv.,1991.[DART-27].∗[Gammelgaard2]A.Gammelgaard,

“Reuseofinvariantsinproofsofimplementation,”

TechnicalMonographDAIMIPB-360,ComputerScienceDept.,AarhusUniv.,1991.[DART-28].∗[GammelgaardLovengreenRumpSogaardAndersen]A.Gammelgaard,H.H.

Løvengreen,C.0.Rump,andJ.F.Søgaard-Andersen,“Basesystemverification.”

Submittedforpublication,1992.IDART-29].∗[GlindtvadNielson]K.GlindtvadandH.R.Nielson,

“CorrectnesspreservingtransformationsonamultipassOCCAMcom-piler,”

35

TechnicalMonographDAIMIPB-368,ComputerScienceDept.,AarhusUniv.,1991.[DART-30].

[GluckKlimov]R.Gl¨uckandA.V.Klimov,

“Occam’srazorinmetacomputation:thenotionofaperfectprocesstree,”

inStaticAnalysis.Proceedings(P.Cousot,M.Falaschi,G.File,andA.Rauzy,eds.),vol.724ofLectureNotesinComputerScience,pp.112-123,Springer-Verlag,1993.[DART-177].[GodskesenLarsen1]J.C.GodskesenandK.G.Larsen,

“Realtimecalculiandexpansiontheorems(extendedabstract),”

inProceedingsoftheFirstNorthAmericanProcessAlgebraWorkshop,Dept.ofComp.Sc,TheJohnsHopkinsUniversity,1992.[DART-157].[GodskesenLarsen2]J.C.GodskesenandK.G.Larsen,

“Realtimecalculiandexpansiontheorems,”

inProceedingsofFST-TCS’92,vol.652ofLectureNotesinComputerScience,Springer-Verlag,1992.[DART-31].[Gomard1]C.K.Gomard,

ProgramAnalysisMatters.

PhDthesis,DIKU,UniversityofCopenhagen,Denmark,1991.DIKUreport91/17.[DART-32].[Gomard2]C.K.Gomard,

“Aself-applicablepartialevaluatorforthelambdacalculus:Correctnessandpragmatics,”

TOPLAS,vol.14,no.2,pp.147-172,1992.[DART-33].∗[GomardJones]C.K.GomardandN.D.Jones,

“Apartialevaluatorfortheun-typedlambdacalculus,”

JournalofFunctionalProgramming,vol.1,pp.21-69,1991.[DART-34].∗[GomardSestoft1]C.K.GomardandP.Sestoft,

“Evaluationorderanalysisforlazydatastructures,”

inFunctionalProgramming,GlasgowWorkshop1991(Heldal,Holst,andWadler,eds.),pp.112-127,Springer-Verlag,1991.[DART-35].[GomardSestoft2]C.K.GomardandP.Sestoft,

“Globalizationandlivevariables,”

36

inProceedingsoftheSymposiumonPartialEvaluationandSemantics-BasedProgramManipulation,SIGPLANNOTICESvol.26,no.9,pp.166-177,ACMPress,1991.[DART-36].

[GomardSestoft3]C.K.GomardandP.Sestoft,

“Pathanalysisforlazydatastructures,”

inProgrammingLanguageImplementationandLogicProgramming,4thInternationalSymposium,PLILP’92,Leuven,Belgium(M.BruynoogheandM.Wirsing,eds.),vol.631ofLectureNotesinCom-puterScience,pp.54-68,Springer-Verlag,1992.[DART-37].[GrooteHuttel]J.F.GrooteandH.H¨uttel,

“Undecidableequivalencesforbasicprocessalgebra,”

Tech.Rep.ECS-LFCS-91-169,DepartmentofComputerScience,Uni-versityofEdinburgh,1991.[DART-38].[Grue]K.Grue,

“Maptheory,”

TheoreticalComputerScience,vol.102,pp.1-133,1991.[DART-39].[GurrBrown1]D.GurrandC.Brown,

“Relationsandnon-commutativelinearlogic,”

TechnicalMonographDAIMIPB-372,ComputerScienceDept.,AarhusUniv.,1991.[DART-40].[GurrBrown2]D.GurrandC.Brown,

“Arepresentationtheroremforquantales.”

ToappearinJounalofPure&AppliedAlgebra,1992.[DART-41].[HankinMetayerSands]C.Hankin,D.L.Metayer,andD.Sands,

“Aparallelprogrammingstyleanditsalgebraofprograms,”

inProceedingofParallelArchitecturesandLanguagesEurope(PARLE),vol.694ofLectureNotesinComputerScience,pp.367-378,Springer-Verlag,1993.Toappear.[DART-178].[Hannan1]J.Hannan,

“Makingabstractmachineslessabstract,”

inProceedingsofthe5thACMConferenceonFunctionalProgrammingandComputerArchitecture(J.Hughes,ed.),vol.523ofLectureNotesinComputerScience,pp.618-635,Springer-Verlag,1991.[DART-42].

37

[Hannan2]J.Hannan,

“Stagingtransformationsforabstractmachines,”

inProceedingsoftheACMSIGPLANSymposiumonPartialEvaluationandSemanticsBasedProgramManipulation(P.HudakandN.Jones,eds.),pp.130-141,ACMPress,1991.[DART-43].[Hannan3]J.Hannan,

“Implementingλ-calculusreductionstrategiesinextendedlogicpro-gramminglanguages,”

inProceedingsoftheSecondWorkshopInternationalWorkshoponEx-tensionsofLogicProgramming(L.-H.Eriksson,L.Halln¨as,andP.Schroeder-Heister,eds.),no.596inLectureNotesinComputerScience,pp.193-219,Springer-Verlag,1992.[DART44].[HannanMiller]J.HannanandD.Miller,

“Fromoperationalsemanticstoabstractmachines,”

MathematicalStructuresinComputerScience,vol.2,1992.Toappear.[DART-45].[HannanPfenning]J.HannanandF.Pfenning,

“CompilerverificationinLF,”

inProceedingsoftheSeventhAnnualIEEESymposiumonLogicinCom-puterScience(A.Scedrov,ed.),IEEEComputerSocietyPress,1992.[DART-46].[HavelundLarsen]K.HavelundandK.G.Larsen,

“Theforkcalculus,”

tech.rep.,AalborgUniversity,Dept.ofMath.andComp.Sc.,1993.[DART-159].[Henglein1]F.Henglein,

“Efficienttypeinferenceforhigher-orderbinding-timeanalysis,”

inFPCA(J.Hughes,ed.),vol.523ofLectureNotesinComputerScience,pp.448-472,5thACMConference,Cambridge,MA,USA,Springer-Verlag,1991.[DART-47].[Henglein2]F.Henglein,

“Typeinferencewithpolymorphicrecursion,”

ACMTransactionsonProgrammingLanguages(TOPLAS),1991.[DART-48].∗

38

andSystems

[Henglein3]F.Henglein,

“Dynamictyping,”

inProc.EuropeanSymp.onProgramming(ESOP),Rennes,France(B.Krieg-Br¨uckner,ed.),vol.582ofLectureNotesinComputerScience,pp.233-253,Springer-Verlag,1992.[DART-49].[Henglein4]F.Henglein,

“Globaltaggingoptimizationbytypeinference,”

inProc.1992ACMConf.onLISPandFunctionalProgramming(LFP),SanFrancisco,California,ACMPress,1992.[DART-50].[Henglein5]F.Henglein,

“Dynamictyping:Syntaxandprooftheory,”

ScienceofComputerProgramming,1993.SpecialIssueonEuropeanSymposiumonProgramming1992(toappear).[DART-179].[HengleinJorgensen]F.HengleinandJ.Jørgensen,

“Formallyoptimalboxing.”

acceptedforPOPL’94,1993.[DART-192].

[HolmerLarsenYi]U.Holmer,K.G.Larsen,andW.Yi,

“Decidabilityofbisimulationequivalencebetweenregulartimedpro-cesses,”

inProceedingsofCAV’91,vol.575ofLectureNotesinComputerSci-ence,1992.[DART-51].[HolstGomard]C.K.HolstandC.K.Gomard,

“Partialevaluationisfullerlaziness,”

inProceedingsofSymposiumonPartialEvaluationandSemantics-BasedProgramManipulation,SIGPLANNOTICESvol.26,no.9,pp.223-233,ACMPress,1991.[DART-52].[HudakJones]P.HudakandN.Jones,

eds.,ProceedingsoftheSymposiumonPartialEualuationandSemantics-BasedProgramManipulation(PEPM),NewHaven,Con-necticut,

SponsoredbytheACMSpecialInterestGroupSIGPLAN,incoopera-tionwithIFIP,ACMPress,1991.[DART-53].

39

[Huttel1]H.H¨uttel,

“Decidability,behaviouralequivalencesandinfinitetransitiongraphs,”ECS-LFCS-91-191,DepartmentofComputerScience,UniversityofEd-inburgh,1992.[DART-54].[Huttel2]H.H¨uttel,

“Silenceisgolden:Branchingbisimilarityisdecidableforcontext-freeprocesses,”

inProceedingsofCAV91,vol.575ofLectureNotesinComputerSci-ence,Springer-Verlag,1992.ThefullversionisavailableasTech.Rep.ECS-LFCS-91-173,DepartmentofComputerScience,UniversityofEd-inburgh.[DART-55].[HuttelChristensenStirling]H.H¨uttel,S.Christensen,andC.Stirling,

“Bisimulationequivalenceisdecidableforallcontext-freeprocesses,”inCONCUP92(W.Cleaveland,ed.),vol.630ofLectureNotesinCom-puterScience,pp.138-147,Springer-Verlag,1992.[DART-156].[HuttelLarsen]H.H¨uttelandK.G.Larsen,

“Adynamictypesystemforhigher-orderprocesses.”AalborgTechnicalreportR93-2003,1992.[DART-155]

[HuttelStirling]H.H¨uttelandC.Stirling,

“Actionsspeaklouderthanwords:Provingbisimilarityforcontext-freeprocesses,”

inProceedingsof6thAnnualSymposiumonLogicinComputerScience(LICS91),pp.376-386,IEEEComputerSocietyPress,1991.[DART-56].[IngolfsdottirSteffen]A.IngolfsdottirandB.Steffen,

“Characteristicformulae,”

InformationandComputation,1992.Toappear.[DART-57].

[IngolfsdottirThomsen]A.IngolfsdottirandB.Thomsen,

“SemanticsmodelsforCCSwithvalues,”

InProceedingsoftheWorkshoponConcurrency,B˚astad,Sweden,1991.[DART-58].[Jensen]C.T.Jensen,

“Theconcurrencyworkbenchwithpriorities,”

40

inProceedingsofCAV’91,Aalborg,Denmark,vol.575ofLectureNotesinComputerScience,Springer-Verlag,1992.[DART-59].

[Jones1]N.D.Jones,

“ComputerimplementationandapplicationsofKleene’ss-m-nandre-cursivetheorems,”

inLectureNotesinMathematics,LogicFromComputerScience(Y.Moschovakis,ed.),pp.243-263,Springer-Verlag,1991.[DART-60].∗[Jones2]N.D.Jones,

“Efficientalgebraicoperationsonprograms,”

inPreliminaryProceedings,UniversityofIowa(T.Rus,ed.),1991.Ac-ceptedforpublicationbyTheoreticalComputerScience,1992.[DART-61].[Jones3]N.D.Jones,ed.,

SelectedPapersofESOP’90.ScienceofComputerProgramming.Vol-ume17,numbers1-3,pages1-271,Elsevier,1991.[DART-62].∗[Jones4]N.D.Jones,

“Staticsemantics,typesandbindingtimeanalysis,”

inImagesofProgramming(D.BjørnerandV.Kotov,eds.),North-Holland,1991.FurtherappearedinTheoreticalComputerScience90(1991),pages95-118.[DART-63].[Jones5]N.D.Jones,

“Constanttimefactorsdomatter,”

inSTOC’93.SymposiumonTheoryofComputing(S.Homer,ed.),ACM,1993.[DART-151].[Jones6]N.D.Jones,

“Partialevaluationandthegenerationofprogramgenerators.”

AcceptedtoappearinCommunicationsofTheACM,1993.[DART-136].[Jones7]N.D.Jones,ed.,

SpecialissueonPartialEvaluation,1993(JournalofFunctionalPro-gramming,vol.?,no.?),

CambridgeUniversityPress,1993.5acceptedpapersbeingrevised;tobeprintedin1993.[DART-152].

41

[JonesGomardSestoft]N.D.Jones,C.Gomard,andP.Sestoft,

PartialEvaluationandAutomaticProgramGeneration.

InternationalSeriesinComputerScience:PrenticeHallInternational,1993.SerieseditorC.A.R.Hoare.ISBNnumber0-13-20249-5(pbk).[DART-180].[JonssonLarsen1]B.JonssonandK.G.Larsen,

“Onthecomplexityofequationsolvinginprocessalgebra,”

inProceedingsofTAPSOFT’91,vol.493ofLectureNotesinComputerScience,Springer-Verlag,1991.[DART-64].[JonssonLarsen2]B.JonssonandK.G.Larsen,

“Specificationandrefinementofprobabilisticprocesses,”inProceedingsofLICS’91,1991.[DART-65].

[Jorgensen1]J.Jørgensen,

“Compilergenerationbypartialevaluation,”

Master’sthesis,DIKU,UniversityofCopenhagen,Denmark,1991.[DART-66].[Jorgensen2]J.Jørgensen,

“Generatingacompilerforalazylanguagebypartialevaluation,”

inNineteenthAnnualACMSIGACT-SIGPLANSymposiumonPrinci-plesofProgrammingLanguages.Albuquerque,NewMexico,pp.258-268,1992.[DART-67].[KlarlundSchwartzbach]N.KlarlundandM.I.Schwartzbach,

“Graphtypes,”

inProc.POPL’93,PrinciplesofProgrammingLangauges,(Charleston),ACM,1993.[DART-143].[KozenPalsbergSchwartzbach1]D.Kozen,J.Palsberg,andM.I.

Schwartzbach,

“Efficientinferenceofpartialtypes,”

inProc.FOCS’92,33rdIEEESymposiumonFoundationsofComputerScience,Pittsburgh,Pennsylvania,1992.AlsoavailableasTech.Rep.DAIMIPB-394,ComputerScienceDepartment,AarhusUniversity.[DART-68].

42

[KozenPalsbergSchwartzbach2]D.Kozen,J.Palsberg,andM.I.

Schwartzbach,

“Efficientrecursivesubtyping,”

TechnicalMonographDAIMIPB-405,ComputerScienceDept.,AarhusUniv.,1992.[DART-69].[Krishnan1]P.Krishnan

“DistributedCCS,”

inProc.CONCUR-91,vol.527ofLectureNotesinComputerScience,pp.393-407,Springer-Verlag,1991.[DART-70].∗[Krishnan2]P.Krishnan,

“Amodelforreal-timesystems,”

inProc.MFCS’91,vol.520ofLectureNotesinComputerScience,Springer-Verlag,1991.[DART-71].∗[Krishnan3]P.Krishnan,

“Real-timeaction,”

inProc.EuromicroWorkshoponRealTimeSystems,l991.[DART-72].∗[Krishnan4]P.Krishnan,“Asemanticsformultiprocessorsystems,”

inESOP’92,Proc.EuropeanSymposiumonProgramming,Rennes,vol.582ofLectureNotesinComputerScience,Springer-Verlag,1992.[DART-73].[KrishnanMosses]P.KrishnanandP.D.Mosses,

“Specifyingasynchronoustransferofcontrol,”

inRTFT’92,Proc.Symp.onFormalTechniquesinReal-TimeandFault-TolerantSystems,Delft,vol.571ofLectureNotesinComputerScience,Springer-Verlag,1992.[DART-74].[Lange]T.P.Lange,

“Thecorrectnessofanoptimizedcodegeneration,”

inPEPM’93,ACMSIGPLANSymposiumonPartialEvaluationandSemantics-BasedProgramManipulation,pp.167-178,ACM,1993.[DART-132].[Larsen1]K.G.Larsen,

“ProofsystemsforsatisfiabilityinHennessy-Milnerlogicwithrecur-sion,”

TheoreticalComputerScience,vol.72,1990.[DART-75].

43

[Larsen2]K.G.Larsen,

“Theexpressivepowerofimplicitspecifications,”

inProceedingsofICALP’91,vol.510ofLectureNotesinComputerSci-ence,Springer-Verlag,1991.[DART-76].[Larsen3]K.G.Larsen,

“Efficientlocalcorrectnesschecking,”

InProceedingsofCAV’92.ToappearinLectureNotesinComputerScience.,1992.[DART-77].[LarsenSkou1]K.G.LarsenandA.Skou,

“Bisimulationthroughprobabilistictesting,”

InformationandComputation,vol.94,no.1,1991.[DART-78].[LarsenSkou2]K.G.LarsenandA.Skou,

“Compositionalverificationofprobabilisticprocesses,”

inProceedingsofCONCUR’92,vol.630ofLectureNotesinComputerScience,Springer-Verlag,1992.[DART-79].[LarsenXinxin]K.G.LarsenandL.Xinxin,

“Compositionalitythroughanoperationalsemanticsofcontexts,”

JournalofLogicandComputation,vol.1,no.6,pp.761-795,1991.[DART-80].∗[LarsenYi]K.G.LarsenandW.Yi,

“Timeabstractedbisimulation:Implicitspecificationsanddecidability,”tech.rep.,AalborgUniversity,Dept.ofMath.andComp.Sc.,1993.[DART-158].[LarsenSchmidtSchwartzbach]K.S.Larsen,E.M.Schmidt,andM.I.

Schwartzbach,

“Anewformalismforrelationalalgebra,”

InformationProcessingLetters,vol.41,no.3,1992.[DART-81].[Malmkjaer1]K.Malmkjær,

“Predictingpropertiesofresidualprograms,”

inPEPM’92,ACMSIGPLANWorkshoponPartialEvaluationandSemantics-BasedProgramManipulation(C.Consel,ed.),pp.8-13,1992.AvailableasTechnicalReportYALEU/DCS/RR-909fromYaleUniver-sity.[DART137].

44

[Malmkjaer2]K.Malmkjær,

“Towardsefficientpartialevaluation,”

inACMSIG-PLANSymposiumonPartialEvaluationandSemanticsBasedProgramManipulation,1993.Toappear.[DART-150].[MarquardSteensgaard]M.MarquardandB.Steensgaard,

“Partialevaluationofanobject-orientedimperativelanguage,”

Master’sthesis,UniversityofCopenhagen,DepartmentofComputerScience,Universitetsparken1,2100CopenhagenO.,Denmark,1992.[DART-138].[MarriotSondergaardJones]K.Marriot,H.Søndergaard,andN.Jones,

“Denotationalabstractintrepretationoflogicprograms,”

ACMTransactionsonProgrammingLanguagesandSystems,1991.Toappear.[DART-82].[MilnerTofte]R.MilnerandM.Tofte,

“Co-inductioninrelationalsemantics,”

TheoreticalComputerScience,vol.87,pp.209-220,1991.[DART-144].∗[Mogensen1]T.Æ.Mogensen,

“Efficientself-interpretationinlambdacalculus,”

FunctionalProgramming,vol.2,pp.345-364,1992.[DART-149].[Mogensen2]T.Æ.Mogensen,

“Efficientself-interpretationinlambdacalculus.”

VersionofDART-149withfullproofs,1992.[DART-83].

[Mogensen3]T.Æ.Mogensen,

“Self-applicablepartialevaluationforpurelambdacalculus,”

inACMSIGPLANWorkshoponPartialEvaluationandSemantics-basedProgramManipulation(C.Consel,ed.),pp.116-121,ACM,YaleUniversity,1992.[DART-84].[Mogensen4]T.Æ.Mogensen,

“Constructorspecialization,”

inACMSymposiumonPartialEualuationandSemantics-BasedPro-gramManipulation(D.Schmidt,ed.),ACMpress,1993.Toappear.[DART-148].

45

[MogensenBondorf]T.Æ.MogensenandA.Bondorf,

“Logimix:aself-applicablepartialevaluatorforProlog,”

inProceedingsofLOPSTR92.WorkshopsinComputing(K.-K.LauandT.Clement,eds.),Springer-Verlag,1993.ISBN:3-540-19806-7.[DART-85].[Mosses1]P.D.Mosses,

“Apracticalintroductiontodenotationalsemantics,”

inFormalDescriptionofProgrammingConcepts(E.J.NeuholdandM.Paul,eds.),IFIPState-of-the-ArtReport,pp.1-49,Springer-Verlag,1991.[DART-87].[Mosses2]P.D.Mosses,

ActionSemantics.

No.26inCambridgeTractsinTheoreticalComputerScience,Cam-bridgeUniversityPress,1992.[DART-88].[Mosses3]P.D.Mosses,

“Ontheactionsemanticsofconcurrentprogramminglanguages,”

TechnicalMonographDAIMIPB-424,ComputerScienceDept.,AarhusUniv.,1992.AcceptedforpublicationinProc.oftheREXWorkshoponSemantics–FoundationsandApplications,Beekbergen,TheNether-lands,June1992.[DART-141].[Mosses4]P.D.Mosses,

“Theoperationalsemanticsofactionnotation,”

TechnicalMonographDAIMIPB-418,ComputerScienceDept.,AarhusUniv.,1992.SubmittedforProc.8thWorkshoponMathematicalFoun-dationsofProgrammingSemantics,whichistoappearasaspecialissueofTCS,1993.[DART-140].[Mosses5]P.D.Mosses,

“Theuseofsortsinalgebraicspecifications,”

inRecentTrendsinDataTypeSpecification(M.BidoitandC.Choppy,eds.),vol.655ofLectureNotesinComputerScience,Springer-Verlag,1992.[DART-139].[Mosses6]P.D.Mosses,

“Anintroductiontoactionsemantics,”

inLogicandAlgebraofSpecification,Proc.MarktoberdorfSummer

46

School1991,vol.94ofNATOASISeriesF,pp.247-288,Springer-Verlag,1993.[DART-86]

[MossesWatt]P.D.MossesandD.A.Watt,

“Pascalactionsemantics,version0.6.”

AvailablebyFTPfromftp.daimi.aau.dkinpub/action/pascal,1993.[DART-162].[Mossin1]C.Mossin,

“Similixbindingtimedebuggermanual,systemversion4.0.”IncludedinSimilixdistribution,1991.[DART-89].

[Mossin2]C.Mossin,

“Partialevaluationofgeneralparsers(extendedabstract),”in1993ACMSymposiumonPartialEvaluationandSemantics-BasedProgramManipulation(D.Schmidt,ed.),1993.Toappear.[DART-147].[Mossin3]C.Mossin,

“Polymorphicbindingtimeanalysis,”

Master’sthesis,DIKU,UniversityofCopenhagen,Denmark,1993.[DART-181].[Musicante]M.A.Musicante,

“TheSunRPClanguagesemantics,”

inProc.18thLatin-AmericanConferenceforInformatics,1992.[DART-90].[MusicanteMosses]M.A.MusicanteandP.D.Mosses,

“Communicativeactionnotationwithsharedstorage,”

TechnicalMonographDAIMIPB-452,ComputerScienceDept.,AarhusUniv.,1993.[DART-163].[MycroftRosendahl]A.MycroftandM.Rosendahl,

“Minimalfunctiongraphsarenotinstrumented,”

inWSA’92Bordeaw1992,pp.60-67,Bigre,Irisa,Rennes,France,1992.[DART-91].[NielsonNielson1]F.NielsonandH.R.Nielson,

“ForcedtransformationsofOCCAMprograms,”

InformationandSoftwareTechnology,vol.34,no.2,1992.[DART-92].∗

47

[NielsonNielson2]F.NielsonandH.R.Nielson,

“Layeredpredicates,”

inREX’92workshop“Semantics-foundationsandapplications”,vol.666ofLectureNotesinComputerScience,pp.425-456,Springer-Verlag,1992.[DART-131].[NielsonNielson3]F.NielsonandH.R.Nielson,

“ThetensorproductinWadler’sanalysisoflists,”

inProceedingsofESOP’92,vol.582ofLectureNotesinComputerSci-ence,Springer-Verlag,1992.[DART-93].[NielsonNielson4]F.NielsonandH.R.Nielson,

Two-LevelBunctionalLanguages,vol.34ofCambridgeTractsinThe-oreticalComputerScience.CambridgeUniversityPress,1992.[DART-94].[NielsonNielson5]F.NielsonandH.R.Nielson,

“Finitenessconditionsforstrictnessanalysis,”

inWSAProceedings,vol.724ofLectureNotesinComputerScience,pp.194-205,Springer-Verlag,1993.[DART-166].[NielsonNielson6]F.NielsonandH.R.Nielson,

“FromCMLtoprocessalgebras,”

TechnicalMonographDAIMIPB-433,ComputerScienceDept.,AarhusUniv.,1993.[DART-165].[NielsonNielson7]F.NielsonandH.R.Nielson,

“FromCMLtoprocessalgebras(extendedabstract),”

inConcur’93,vol.715ofLectureNotesinComputerScience,pp.495-508,Springer-Verlag,1993.[DART-164].[FNielson1]F.Nielson,(ed.),

“Design,analysisandreasoningabouttools:Abstractsfromthefirstworkshop,”

TechnicalMonographDAIMIPB-367,ComputerScienceDept.,AarhusUniv.,1991.[DART-95].[NielsonNielson8]H.R.NielsonandF.Nielson,

“Usingtransformationsintheimplementationofhigher-orderfunc-tions,”

48

JournalofFunctionalProgramming,vol.1,no.4,pp.459-494,1991.[DART-96].∗

[NielsonNielson9]H.R.NielsonandF.Nielson,

“Boundedfixed-pointiteration,”

J.LogicComputat.,vol.2,no.4,pp.441-464,1992.[DART-134].[NielsonNielson10]H.R.NielsonandF.Nielson,

“Boundedfixedpointiteration,”

inProceedingsofPOPL’92,ACMPress,1992.Thisisan“extendedabstract”ofDART-134.[DART-97].[NielsonNielson11]H.R.NielsonandF.Nielson,

“Finitenessconditionsforfixedpointiteration”

inProceedingsofLispandFunctionalProgramming,1992.Thefullver-sionappearedasDAIMIPB-384,AarhnsUniversity.lDART-98].[NielsonNielson12]H.R.NielsonandF.Nielson,

SemanticswithApplications:AFormalIntroduction.Wiley,1992.[DART-99].[NielsonNielson13]H.R.NielsonandF.Nielson,

“Iterativealgorithmsforfixedpointcomputation,”

TechnicalMonographDAIMIPB-441,ComputerScienceDept.,AarhusUniv.,1993.[DART-160].[NielsonNielsonPilegaardLange]H.R.Nielson,F.Nielson,A.Pilegaard,and

T.Lange,

“ThePSIsystem,”

InternalReportDAIMIIR-114,ComputerScienceDept.,AarhusUniv.,1992.[DART-130].[FNielson2]F.Nielson,(ed.),

“Design,analysisandreasoningabouttools:Abstractsfromthesecondworkshop,”

TechnicalMonographDAIMIPB-417,ComputerScienceDept.,AarhusUniv.,1992.[DART-100].[OxhojPalsbergSchwartzbach]N.

Schwartzbach,

Oxhøj,

J.

Palsberg,

and

M.

I.

49

“Makingtypeinferencepractical,”

inProc.ECOOP’92,SixthEuropeanConferenceonObject-OrientedProgramming,Utrecht,TheNetherlands,vol.615ofLectureNotesinComputerScience,pp.329-349,Springer-Verlag,1992.[DART-101].[Palsberg1]J.Palsberg,

“AnautomaticallygeneratedandprovablycorrectcompilerforasubsetofAda,”

inICCL’92,Proc.FourthIEEEInt.Conf.onComputerLanguages,Oakland,pp.117-126,IEEE,1992.[DART-102].[Palsberg2]J.Palsberg,

ProvablyCorrectCompilerGeneration.

PhDthesis,AarhusUniversity,1992.[DART-103].

[Palsberg3]J.Palsberg,

“Aprovablycorrectcompilergenerator,”

inESOP’92,Proc.EuropeanSymposiumonProgramming,Rennes,vol.582ofLectureNotesinComputerScience,pp.418-434,Springer-Verlag,1992.[DART-104].[PalsbergKozenSchwartzbach]J.Palsberg,D.Kozen,andM.I.

Schwartzbach,

“Efficientrecursivesubtyping,”

inProc.POPL’93,PrinciplesofProgrammingLangauges,(Charleston),ACM,1993.[DART-142].[PalsbergSchwartzbach1]J.Palsberg,andM.I.Schwartzbach,

“Object-orientedtypeinference,”

inProc.OOPSLA’91,ACMSIGPLANSixthAnnualConferenceonObject-OrientedProgrammingSystems,LanguagesandApplications,Phoenix,Arizona,pp.146-161,1991.[DART-105].[PalsbergSchwartzbach2]J.Palsberg,andM.I.Schwartzbach,

“Statictypingforobject-orientedprogramming,”

TechnicalMonographDAIMIPB-355,ComputerScienceDept.,AarhusUniv.,1991.[DART-106].[PalsbergSchwartzbach3]J.Palsberg,andM.I.Schwartzbach,

“Types,inheritanceandassignments,”

50

1991.WorkshopheldatECOOP’91inGeneva,Switzerland,July1991.ThecollectionofpositionpapersisavailablefromComputerScienceDepartment,AarhusUniversityasPB-357.[DART-107].

[PalsbergSchwartzbach4]J.Palsberg,andM.I.Schwartzbach,

“Whatistype-safecodereuse?,”

inProc.ECOOP’91,FifthEuropeanConferenceonObject-OrientedProgramming,Geneva,Switzerland,vol.512ofLectureNotesinCom-puterScience,pp.325-341,Springer-Verlag,1991.[DART-108].[PalsbergSchwartzbach5]J.Palsberg,andM.I.Schwartzbach,

“Safetyanalysisversustypeinference,”

TechnicalMonographDAIMIPB-389,ComputerScienceDept.,AarhusUniv.,1992.[DART-109].[PalsbergSchwartzbach6]J.Palsberg,andM.I.Schwartzbach,

“Safetyanalysisversustypeinferenceforpartialtypes,”

InformationProcessingLetters,vol.43,pp.175-180,1992.AlsoavailableasTech.Rep.DAIMIPB-404,ComputerScienceDepartment,AarhusUniversity.[DART-110].[PalsbergSchwartzbach7]J.Palsberg,andM.I.Schwartzbach,

“Threediscussionsonobject-orientedtyping,”

ACMSIGPLANOOPSMessenger,vol.3,no.2,pp.31-38,1992.[DART-111].[RehofSorensen]J.RehofandM.H.Sørensen,

“Theλδ-calculus.”

TechnicalreportfromDIKU,1993.[DART-182].

[Rose1]K.H.Rose,

“Explicitcyclicsubstitutions,”

inCTRS’92–3rdInternationalWorkshoponConditionalTermRewrit-ingSystems(M.RusinowitchandJ.-L.R´emy,eds.),no.656inLec-tureNotesinComputerScience,(Pont-a-Mousson,France),pp.36-50,Springer-Verlag,1992.AlsoavailableasDIKUsemanticsnoteD-143.[DART-113].[Rose2]K.H.Rose,

“GOS-graphoperationalsemantics,”

51

M.Sc.-thesis92-1-9,DIKU,UniversityofCopenhagen,Denmark,1992.AwardedasilvermedalbytheUniversityofCopenhagen.[DART-114].[Rose3]K.H.Rose,

“Graph-basedoperationalsemanticsforlazyfunctionallanguages,”inTermGraphRewriting:TheoryandPractice(M.R.Sleep,M.J.Plasmeijer,andM.vanEekelen,eds.),(Nijmegen,Holland),pp.203-225,JohnWiley&Sons,1992.[DART-112].[Rose4]K.H.Rose,

“Graph-basedoperationalsemanticsofalazyfunctionallanguages,”inTermGraphRewriting:TheoryandPractice(M.R.Sleep,M.J.Plasmeijer,andM.C.D.J.vanEekelen,eds.),ch.22,pp.234-247.JohnWiley&Sons.1992.[DART-183].[Rose5]K.H.Rose,

“HowtotypesetprettydiagramarrowswithTEX—designdecisionsusedinXY-pic,”

inEuroTEX’92—Proceedingsofthe7thEuropeanTEXConference(J.Zlatuska,ed.),(Prague,Czechoslovakia),pp.183190,CzechoslovakTEXUsersGroup,1992.[DART-173].[Rose6]K.H.Rose,

“Explicitcyclicsubstitution.”

SelectedforspecialissueofJournalofSymbolicComputation,1993.[DART-184].[Rose7]K.H.Rose,

“Explicitrecursion.”

AvailableasDIKUsemanticsnoteD-147,1993.[DART-185].[Rosendahl1]M.Rosendahl,

AbstractInterpretationandAttributeGrammars.

PhDthesis,CambridgeUniversity,1991.[DART-172].

[Rosendahl2]M.Rosendahl,

“Strictnessanalysisforattributegrammars,”

inPLILP’92,vol.631ofLectureNotesinComputerScience,pp.145-157,Springer-Verlag,1992.[DART-115].

52

[Rosendahl3]M.Rosendahl,

“Higher-orderchaoticiterationsequences,”

inPLILP’93,Tallinn,Estonia,no.714inLectureNotesinComputerScience,pp.332-345,Springer-Verlag,1993.[DART-193].[Sands1]D.Sands,

“AcompositionalsemanticsofcombiningformsforGammaprograms,”inInternationalConferenceonFormalMethodsinProgrammingandTheirApplications.,LectureNotesinComputerScience,1993.[DART-187].[Sands2]D.Sands,

“Lawsofparallelsynchronisedtermination,”

inTheoryandFormalMethods1993:ProceedingsoftheFirstImperialCollege,DepartmentofComputing,WorkshoponTheoryandFormalMethods(G.Burn,S.Gay,andM.Ryan,eds.),(IsleofThorns,UK),Springer-VerlagWorkshopsinComputerScience,29-31March1993.[DART-188].[Sands3]D.Sands,

“Ana¨ıvetimeanalysisanditstheoryofcostequivalence.”

SubmittedforpublicationatDIKU,Copenhagen,1993.Canbeobtainedbyftpfromsiteftp.diku.dkinsemantics/papers/D-173.ps,dvi.[DART-186].[Schwartzbach]M.I.Schwartzbach,

“Typeinferencewithinequalities,”

inProc.TAPSOFT’91,vol.493ofLectureNotesinComputerScience,Springer-Verlag,1991.[DART-116].[Sestoft]P.Sestoft,

Analysisandefficientimplementationoffunctionalprograms.

PhDthesis,DIKU,UniversityofCopenhagen,Denmark,1991.DIKUResearchReport92/6.[DART-117].[Solberg]K.L.Solberg,

“Inferencesystemsforbindingtimeanalysis,”

Tech.Rep.25,OdenseUniversity,1993.[DART-161].

53

[SolbergNielsonNielson]K.L.Solberg,H.R.Nielson,andF.Nielson,

“Inferencesystemsforbindingtimeanalysis(extendedabstract),”

inWSA’92:Work-shoponStaticAnalysis,Bigreno.81-82,pp.247-254,UniversityofBordeaux,1992.[DART-135].[SondergaardSestoft]H.SøndergaardandP.Sestoft,

“Non-determinisminfunctionallanguages,”

ComputerJournal,vol.35,pp.514-523,1992.[DART-118].

[SorensenClausen]B.B.SørensenandC.Clausen,

“Adequacyresultsforalazyfunctionallanguagewithrecursiveandpolymorphictypes,”

InternalReportDAIMIIR-113,ComputerScienceDept.,AarhusUniv.,1992.SubmittedtoTheoreticalComputerScience.[DART-119].[Sorensen]M.H.Sørensen,

“Anewmeansofensuringterminationofdeforestation.”

AcceptedfortheWorkshopofGlobalCompilationinconnectionwiththeInternationLogicProgrammingSymposium,1993,Vancouver,Canada.Copiesavailablefromtheauthor(atDIKU).,1993.[DART-190].[Tofte1]M.Tofte,

“CodegenerationusingstandardML.”

LecturenotesfromDIKU,1991.[DART-170].

[Tofte2]M.Tofte,

“TutorialonstandardML,”

Tech.Rep.91/18,DIKU,UniversityofCopenhagen,Denmark,1991.PresentedatFPCA,Boston,1991.[DART-171].[Tofte3]M.Tofte,

“Principalsignaturesforhigher-orderprogrammodules,”

inThe19thAnnualACMSymposiumonPrinciplesofProgrammingLanguages,Albuquerque,NewMexico,pp.189-199,1992.[DART-120].[TofteTalpin1]M.TofteandJ.-P.Talpin,

“Atheoryofstackallocationinpolymophicallytypedlanguages,”

Tech.Rep.DIKU-report93/15,DIKU,UniversityofCopenhagen,Den-mark,1993.[DART-195].

54

[TofteTalpin2]M.TofteandJ.-P.Talpin,

“Implementationofthetypedcall-by-valuelambda-calculususingastackofregions,”

inProceedingsfromthe21stannualACMSIGPLAN-SIGACTSym-posiumonPrinciplesofProgrammingLanguages,1994.(Acceptedforpublication).[DART-196].[Winskel1]G.Winskel,

“Onlocalmodelcheckingthemodalν-calculus,”

1991.IntheICALP’89,specialissueofTheoreticalComputerScience,vol.83,1991.[DART-121].[Winskel2]G.Winskel,ed.,

CLICSWorkshop-PartsIandII.ProceedingsoftheWorkshoponCat-egoricalLogicinComputerScience,1992.

Alsoavailablea.sTech.Rep.DAIMIPB-397IandII,ComputerScienceDepartement,AarhusUniversity.[DART-122].[Winskel3]G.Winskel,

Theformalsemanticsofprogramminglanguages.MITPress,1993.[DART-123].[WinskelCamilleri]G.WinskelandJ.Camilleri,

“CCSwithaprioritychoice,”

inProceedingsofLICS,1991.[DART-124].

[WinskelLarsen]G.WinskelandK.Larsen,

“Usinginformationssystemstosolverecursivedomainequations,”InformationandComputation,vol.91,no.2,1991.[DART-125].∗[WinskelNielsen]G.WinskelandM.Nielsen,

“Modelsforconcurrency.”

ToappearasachapterintheHandbookofLogicandtheFoundationsofComputerScience,OxfordUniversityPress.[DART-126].[Xinxin]L.Xinxin,

SpecificationandDecompositioninConcurrency.

PhDthesis,DepartmentofMathematicsandComputerScience,Aal-borgUniversity,Denmark.,1992.[DART-127].

55

[YiLarsen]W.YiandK.G.Larsen,

“Testingprobabilisticandnondeterministicprocesses,”ProceedingsofPSTV’92,1992.[DART-128].

56