New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here

Programming Languages

by: Nick Rowe

Programming Languages CS 56500

Nick Rowe
GPA 3.68

Suresh Jagannathan

Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Suresh Jagannathan
Class Notes
25 ?




Popular in Course

Popular in ComputerScienence

This 33 page Class Notes was uploaded by Nick Rowe on Saturday September 19, 2015. The Class Notes belongs to CS 56500 at Purdue University taught by Suresh Jagannathan in Fall. Since its upload, it has received 42 views. For similar materials see /class/208075/cs-56500-purdue-university in ComputerScienence at Purdue University.

Similar to CS 56500 at Purdue

Popular in ComputerScienence


Reviews for Programming Languages


Report this Material


What is Karma?


Karma is the currency of StudySoup.

You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 09/19/15
CS 565 Programming Languages Spring 2009 MWF 130 220 Lawson 1106 AdminisTrivia El Who am I El Course Web Page I hTTplwwwcspurdueeduhomesSureSh565Spring2009 El Office Hours l Tu Th 2 3 PM I By appointment El Main Tex r l Types and Programming Languages B Pierce MIT Press Course Work LecTures Homeworks l Periodic probably one every Two weeks or so I The answers To some of The quesTions will be available in The back of The TexT l CollaboraTing on homework encouraged Programming Exercises I Will involve implemenTing Type checkers and inTerpreTers l Code size for soluTions will be small lt 250 lines buT soluTions will be challenging A midTerm CumulaTive final which will also serve as The qualifying exam Prerequis res III Programming experiencematurity l exposure To various language consTrucTs El Java ML Lisp Prolog C Undergradua re compilers andor PL class El CS 352 andor CS 456 or equivalent III Ma rhema rical ma ruri ry l familiariTy wiTh firsTorder logic seT Theory graph Theory inducTion III Mos r impor ran r l In rellec rual curiosi ry and creaTiviTy Resources El Web page for Text I hTTpwwwcisupennedubcpierceTop El SupplemenTory moTerial l hTTDwww2immdTudkriisPPApDosuDZOO4hTm Web page for ML implemenToTions hTTpcominriofr Coml hTTpwwwsmn jorg SMLNJ hTTDwwwmlfonora MLTon Proceedings of conferences l POPL PLDI ICFP Background El Our main goal is To find ways To describe The behavior of programs precisely and concisely El Mo riva rion l Significan r indus rry and governmen r in reres r III Web Java III SecuriTy issues III Complexi ry of modernday applica rions Mo riva rion con r El Prove specific fac rs abou r programs I Verify correcTness III Impor ran r in missioncriTical sys rems l Safe ry or isola rion proper ries I Need an unambiguous vocabulary El Unders rand specific language fea rures l BeTTer language design I Guide improvemen rs in implemen ra rions Goals III A more sophisTicaTed appreciaTion of programs Their sTrucTure and The field as a whole Viewing programs as rich formal maThemaTical objecTs noT mere synTax Define and prove rigorous claims abouT a program39s meaning and behavior Develop sound inTuiTions To beTTer judge language properTies El Develop Tools To be beTTer programmers sofTware designers and compuTer scienTisTs Non goals El An in rroduc rion To advanced programming Techniques El No de roiled discussion of machine implemen ro rions l The course will no r be mo rivo red from The perspec rive of a compiler wri rer l Bu r impoc r of design decisions on implemen ro rion rroc robili ry will be considered when opproprio re III A survey of differen r longuoges Topics III Par r I Founda rions Seman ric formalisms k calculus abs rrac r in repre ra rion in rroduc rion ro Types Par r II Design SimplyTyped kcalculus records references sub ryping objec rbased programming Par r III Fea rures Polymorphism abs rrac r da ra rypes advanced Topics eg concurrency lineari ry Par r IV Tools Mechanized me rafheory and proof assis ran rs SemanTics El Three classical approaches l OperaTional III Define programs in Terms of rules ThaT apply To a specific virTual machine III Useful for implemenTing a compiler or inTerpreTer DenoTaTional El Meaning in Terms of funcTions from synTax program TexT To domains values El Useful for describing The behavior of programs I AxiomaTic El Logical rules for reasoning abouT programs El Useful for proving program correcTness AbsTracT InTerpreTaTion El Reason abouT programs by absTracTing away properTies ThaT are noT of inTeresT l Type sysTems l Sign ariThmeTic l Reason abouT The correspondence beTween resulTs produced in The absTracT world wiTh resulTs ThaT would be produced in The concreTe world Case sTudies III Lisp 15 BaSed on kcalculus Key aSpecT of The calculus is noTion of SubSTiTuTion of free variables El funcTion f args x El SuppoSe x is noT included in ar39gs Where Should The binding for39 x be conSTr39ucTed l AT The poinT where f is defined lexical Scoping l AT The poinTS where f is applied dynamic scoping Lisp 15 and laTer39 dialecTs choSe dynamic Scoping even Though iT is widely agr39eed Today ThaT lexical Scoping iS The more Sensible choice When do TheSe diSTincTionS ar39iSe Why are The differences impor39TanT Lack of formal SemanTicS To explore The r39amificaTionS of design choice Case sTudies El l InTeracTion of Types wiTh references I Polymorphism code ThaT works uniformly on all various Types of daTa El lengTh x IisT gt inT El hd 0c lisT gt 0c III TI a IisT gt a IisT Type inference El Assign The mosT general Type To variables based on The conTesz in which They occur Case s rudies ML El References I Like updaTeable poinTer39s in C l Expressions El r39ef e 1 gt1 ref El le 1 ref gt1 III e1 e2 tref1gt1ref fun idx x id a gt x val c r39ef id c 0L gt a rd fun incx x 1 inc im gt im c inc Ok if we infer c inT gt im r39ef c True Ok if we infer c bool gt bool r39ef Case studies Java Ar39r39ay Types B One of Java39s design misTakes is The subTyping rule for39 arrays gt Given ObjecT Types T and I The array subTyping rule is T lt T 3 TH lt2 Ti if T is a subtype of I then T is a subtype of 1quot 1 gt Example String lt2 Object thus St rinau lt1 Obievt Case STudies Java Array Types III STaTic Typing guaranTees ThaT if we have declaraTion T v Then The following holds aT all Times v insTanceof T III This is good because iT guaranTees ThaT Type errors do noT occur aT runTime III Arrays break sTaTic Type safeTy Case S rudies Java Array Types El The following is a s ra ric error Thread appThreads new Thread10 appThreads0 quotbadaboomquot 39rype error Bu r The following is perfectly fine Objec appThreads new Thread10 appThreads0 quotbadaboomquot runFirs rThread Thread appThreads void runFirs rThread Thread 0 o0run run rime Type error Case S rudies Java Array Types Objec appThreads new Thread10 OK Thread lt1 ObjecT appThreadsO quotbadaboomquot OK STring lt Objec r runFirs rThreadThread appThreads appThreads insTanceof Thread void runFirsTThread Thread 0 o0run OK oO is declared To be a Thread The problem is The subTyping rule Case S rudies Java Array Types Why have Tha r rule 9 TO wri re sor Objeci once ra rher Than have To rewri re if for each new class I bu r sub rype polymorphism is a poor subs ri ru re for parameTric polymorphism The righ r solu rion is generici ry sor m implements ComparabieltAgtgt Lessons El Language design is as much abou r safe ry as if is abou r efficiency and expressiveness Need Tools and frameworks To reason abou r and compare differen r language fea rures and designs I unTyped kcalculus as a universal compu ra rion language Precisely define i rs behavior using differenT semanTic models opera rional denoTaTional axiomaTic l Typed kcalculii To express safeTy and absTracTion proper ries Homework El Reading I Chap rerl El Familiarize yourself wi rh ML El Nex r Time I MaThemaTical preliminaries l In rroduc rion To un ryped ari rhme ric l In rroduc rion To Coq Review Slides Boo leans SynTax of Terms and values CS 565 1 7 Terms Final Exam Review Slides 7 true consTanT True fa ls e consTanT false l if 139 then 139 else 139 condl onal values V True value true false false value TransiTion EvaluaTion RelaTion Terminology The relaTion T gt T39 is The smallesT relaTion closed under The following rules I if true then 1392 else 1393 quotl392 I if false then 1392 else 1393quotl 3 I 11 1f 1391 then Td else 1393 39lf 1391 then 1392 else 1393 El CompuTaTion rules I if true then 1392 else 1393 39 1392 I if false then 1392 else 1393 quotl393 El Congruence rule 1 1139 1f 1391 then 1392 else 1393 39 1f 139139 then 1392 else 1393 CompuTaTion rules perform real compuTaTion sTeps Congruence rules guide evaluaTion order They deTermine where compuTaTion rules can be nexT applied IMP A simple imperative language Syntactic categories I Int integers D nez I bool boolean a true false I L locations D xy D Aexp Arithmetic expressions D e I Bexp Booleanexpressions D b I Com Commands D c D Values E v nltrue l false Abstract syntax Comm Commands C Skip I x e c139 c2 I if b then C1 else C2 I while b do C I Typing rules expressed implicitly in the choice of metaVariables All sideeffects captured within commands Do not consider functions pointers data structures I I Operational Semantics for IMP U Unlike the simple language of booleans and conditionals or arithmetic IMP programs bind variables to locations and can sideeffect the contents of these locations D Define a e 2 L gt Z to define the state of program memory D Evaluation judgements take one of the following forms D c 039 gt 0 I t c 39 t39Oquot I t 6 Term Aexp Bexp Com Value Natural Semantics for Corn 60 2h ltxeogt 2 ox l gt n ltskipogt 2 a ltc1ogt 2 a39 ltc2a39gt 2 o c1c2ogt 2 o ltbagt 2 true ltc1ogt 2 a39 ltif b then c1 else 220 2 o39 ltif b then c1 else c2ogt 2 a39 ltbagt 2 false ltbagt 2 true ltc while b do cagt 2 a39 while b do cogt 2 0 while b do cogt 2 a39 ltbagt 2 false ltc2ogt 2 a39 Redex A redex is a Term ThaT can be Transformed in a single sTep I A redex has no anTecedenTs lrxIxnxnnskipcI if True Then c1 else c2 I if false Then c1 else c2 I True A b I false v b I ConTesz EICan define evaluaTion conTexT via a grammar EnEnExE if E Then c1 else c2 I E c I while E do c The grammar fixes The order of evaluaTion allowing us To simplify The number and sTrucTure of The rules used in The semanTics OperaTional SemanTics Lambda Calculus D values The firsT compuTaTion rule is 39 A X T referred To us The subsTiTuTion El CompuTaTion rule or Sconversion rule a x v Tvx A gtlt 1 2 n congruence rules Is called a Sredex 1 139 The IasT congruence rule is 1 T2 quot T139 T2 referred as The nconversion rule I T2 T239 h A X 139 X d w erexnoT in FVT is annre ex v 2 39 v 2 nconversion reIaTed To noTion X quotof free in T of funcTion exTensionaliTy Why A x T x v T Normal forms and order of evaluaTion El No expression can be converTed To Two disTincT normal forms Church Rosser Theorem 1 El Is There an order of evaluaTion guaranTeed To TerminaTe whenever a parTicular expression is reducible To normal form I Normalorder lemeosT ouTermosT reducTion no expression in The argumenT posiTion of a redex is reduced unTiI The redex is reduced I If There is a reducTion from A To B and B is in normal form Then There exisTs a normal order reducTion from A To B Ch urchRosser Theorem 2 Proof Rules Aximoatic Semantics El Skip P SkiP P El Assignment PtxxtP Example Suppose t x 1 Then x12xx1x2 539 Sequencing P 60 Q Q 61 Q39 P 6061 Q39 Proof Rules Scontl El Conditionals PAbCOQPAbC1Q P if b then co else c1Q El Loops PAbcP PwhilebdocPA ub El Con5equence PcQ if l P gt P then all states 0 which satisfy P also satisfy P39 Rule allows strengthening of P to P and weakening of Q to Q Syntax F1 Terms e x hxre I e1 e In e1e2 I iszeroe I true I false I not e I if e1 then e2 else e3 T pes 17 int I bool I 171 12 gt is a function type constructor and associates to the right Formal arguments to functions have typing annotations Static Semantics El The typing judgment F l e 13 El Typing rules xrelquot Fxr er Fl xr FI hxrel r gtr Fl elzrl mz 1quotle2I1 I lelezm2 Static Semantics cont El More typing rules Fl nzint Fl e1int Fl ezint Fl e1e2int Fl true bool Fl e bool Fl notebool Fl e1bool1quote2r1quotl e3r Fl if e1 then e2 else e3zt Operational Semantics of F1 El Evaluation relation l e U v El Values I vn I truelfalselkxzte El Callbyvalue evaluation rules KXVLCUKXI LE e1 U 7 x Lel ez U v2 Vaxe139 U v ez U v Operational Semantics cont More rules elUn1 ernZ nn1nz n U n e1 e2 n e1 U true ef U v if e1 then er else ef U v e1 U false ef U v if e1 then er else ef U v Smal lstep contextual semantics El Define redexes r 1 n1 n2 I if v then e1 else e2 I 9 x T e1 v2 Define contexts E3 1 I Equot39ez I l39IH39EI if E then e else e Eez I hxre1E El Local reduction rules n1 n2 gt me ha if true then e1 else e2 21 if false then e1 else e2 gt e2 9 xzr el v2 gt vZxel Global reduction rule Er gt Ee iff r gt e El El S39la39lic Semantics for Product Types F1x Extend The Semantics with binary 39l39uples e e1 e2 fs r e 5nd e T I 131 x T2 Same Typing judgmenTFl er I l elzr1 I l ezm2 1quotquotepezVHXTz 1quotl er1gtltr2 1 l er1gtltr2 I l fs rezr1 Fl snderz Dynamic Semantics for39 Product Types El New form of values v I v1 v2 El New bigsfep evaluaTion rules e U v e U v 3132 U V1IV2 e U V1V2 M 1 5er1 snderz Typing Rules for Sum Types F l ezr1 F l e 12 1quotlinjlerlr2 1quotl injr39erlr2 1 l e1211r2 1quotxrlle1r 1quotyrzlezzr Fl caseelofinjlxgtellinjrygte2r Dynamic SemanTics El New values v z l injlv injrv El New evaluation rules e U v e U v ind eU ind v injr er e U injl v vxe U v39 caseeof injlxae I injrygterUv39 e U injr v vyJe U v39 caseeo injxgte I injrygterUv39 AnnoTaTions New synTacTic forms e I injleasr I injr39eas caseeofinjlxasre1 injr y as 1 gt e2 17 I 171 172 New Typing rules l l eH1 l l ent2 Phinjleasrlrzirlrz Fl injreasrlrzirlrz Typing and EvaluaTion Rules e I fix e Fl elT1 T2 FFfRen eUAxmd fix e U fix 9 xre39xe39 SubsumpTion Fl eZ00lt17 FI ezr This rule Tells us ThaT if 0 lt2 1 every elemenT v 6 o is also an elemenT of 17 Thus if our subType r elaTion defined x NaT y Bool lt2 x 2 NOT Then The subsumpTion rule would allow us To derive x0yTr ue szaT Arrow Types r1lt 01 02 lt 3952 o102ltrr1rz The subType r elaTion is conTr avar ianT in The Type of The argumenT and covarianT in The Type of The r esulT InTuiTion if we have a funcTion f of Type 01 gt 02 Then we know f accest elemenTs of any subType 3951 lt 01 Since f r eTur ns elemenTs of Type 02 These r esulTs belonq To any superType 3952 of 02 SubTyping References El Try covariance 0 lt31 W U Assume o lt31 I The following holds El xryoreff0 gt inTI yxfy U Unsound f is called on a r buT is defined only on o D If we wanT covariance of references we can recover Type safeTy wiTh a runTime check for each yx assignmenT I The acTual Type of x maTches The acTual Type of y I This is noT a parTicularly good design I NoTe Java has covarianT arrays SubTyping References AnoTher approach conTravariance OCT C ref lt1 0 ref D Assume 0 lt2 The following holds I x21 yzrref f10gtin39l39 Fyxfy I Unsound f is called on a l buT is defined only on 0 El references can be used in Two ways E39 for reading conTexT expecTs a value of Type 0 buT The reference yields a value of Type I Then we need I lt1 0 D for wriTing The new value provided by The conTexT will have Type 0 If The acTual Type of The reference is ref I Then This value may be read and used as a I This will only be safe if 0 lt2 I STaTic SemanTics of Recursive Types l l e Mt 39 l l unfold tj e I MtTt7 l l e I Luffth l l foldlutf e I Lt 39 III The Typing rules are synTax direcTed El OfTen for synTacTic simpliciTy The fold and unfold operaTors are omiTTed I This makes Type checking somewhaT harder Dynamics of Recursive Types D We add a new form of value v fold 4m v I The purpose of fold is To ensure ThaT The value has The recursive Type and noT iTs unfolding III The evaluaTion rules 6 ll 1 6 ll foldMOT v foldMOT 6 ll foldMOT v unfoldMOT 6 ll 1 The folding annoTaTions are for Type checking only They can be dropped afTer Type checking UnTyped Programming El We wriTe e for The conversion of The Term e To Typed 9 calculus wiTh recursive Types F19 l TheTypeofeisVuTT gtT III The conversion rules x x foldv kxV e elez unfoldv 91 9 El VltgtrifI ThaT 1 l g V 2 erifandonlyifeUv New Rules 393 fold and unfold operaTions a lt X I gt uXiIt X H uXJfIt lt 739 oltuXt uXJf lt739 El Amber Rules ZXltYl SltT XltYEE Zl uXSltLLYT El XltY ParameTric Polymorphism Types as ParameTers SysTem F D We inTroduce Type variables and allow expressions To have variable Types D We inTroduce polymorphic Types tbt1 gtr2ITIVTt e x I Mme I e1 e2 I AT e I et I AT e is Type absTracTion or generalizaTion I et is Type applicaTion or insTanTiaTion El Examples I id AT gtltT x VTT gt T I idinT kxnnT x inT gt inT I idbool hxbool x bool gt bool I id 5quot is invalid Use id inT 5quot insTead ImpredicaTive Polymorphism IIThe Typing rules szinl I739le7quot l l QZIT Fl AxiTeIT gtT l leliT gt7quot ll 22739 Fl elegiT l leIT l lte v t739 75 does not occur in F l l e I V717quot l l e739 I Tt7quot PredicaTive Polymorphism El ResTricTion Type variables can be insTanTiaTed only wiTh monomorphic Types E39 This resTricTion can be expressed synTacTically 1b11 gt12T 0rIVT0I01gt02 e x I e1 e2 I Mae I ATe I e 1 I Type applicaTion is resTricTed To mono Types I CannoT apply id To iTself anymore Same Typing rules Simple semanTics and TerminaTion proof Type reconsTrucTion sTill undecidable MusT resTricT furTher El El El El Prenex PredicaTive Polymorphism El ResTricTion polymorphic Type consTrucTor aT Top level only III This resTricTion can also be expressed synTacTically rbr1 gtt2IT O t I VT 0 e x I e1 e2 I Xxx e I ATe I e r I Type applicaTion is resTricTed To mono Types ie predicaTive I AbsTracTion only on mono Types I The only occurrences of V are aT The Top level of a Type VT T gt T gt VT T gt T is M a valid Type D Same Typing rules 393 Simple semanTics and TerminaTion proof El Decidable Type inference ML39s Polymorphic LeT El ML soluTion slighT exTension of The predicaTive F2 I InTroduce leT x 0 e1 in e2quot I WiTh The semanTics of Xx 0e2 e1quot I And Typed as e1x e2quot l lelia l a0l622739 l lletazia 2611116237 D This leTs us wriTe The polymorphic sorT as leT s VTI AT code for polymorph c sorT n s naT X s bool y El Surprise This was a major ML design flaw The Value ResTricTion in ML U A Type in a leT is generalized only for synTacTic values F l 61 0 la 0 l 62 739 61 is a Syntactic value or 0 is l l let a 0 61 1n 62 739 monomorphic El Since e1 is a value iTs evaluaTion cannoT have sideeffecTs D In This case callbyname and callbyvalue are The same III In The previous example ref kxT x is noT a value III This is noT Too resTricTive in pracTice ExisTenTial Types El Provides Two views 39 From The ouTside The acTual r39epr39esenTaTion is hidden or39 opaque 39 From The inside The objecT has The Type defined by The r39epr39esenTaTion 393 Example I The package absType p implemenTs lt a p f p gt p gt is ltpNaTaOfincgt I and hasTypeElTlta Tf T gt T gt El NoTe ThaT a given exisTenTial Type may be associaTed wiTh many differ39enT implemenTaTions El DaTa AbsTracTion IT is useful To separ39aTe The cr39eaTion of The absTr39acT Type and iTs use ExTend The synTax Ter39ms ltT T e o gt open ea as T x o in eb Types I EIT 0 The expression ltT T e O39gtquot Takes The concr39eTe implemenTaTion e and packs iTquot as a value of an absTr39acT Type T wiTh hidden r39epr39esenTaTion Type T and acTual Type 039 The quotopenquot expr39ession allows eb To access The absTr39acT Type expr39ession ea using The name x The unknown Type of The concr39eTe implemenTaTion T Typing Rules for ExisTenTial Types D We add The following Typing rules I l Tte I Tt0 Fl tZTe0gtIElt0 l leaiElto l tp0leb739 l lopeneaastpiainebi739 tgFll UT III The r39esTr39icTion in The rule for open ensures ThaT T does noT escape iTs scope EvaluaTion Rules for AbsTracT Types D We add a new form of value v I lt l391 v 0gt I This is jusT like v buT wiTh some Type decor39aTions ThaT make iT have an exisTenTial Type ea u lt7 m agt vxllTtleb u v39 ATTh open ea as t E I 0 in 65 ll 0 I If we ignore The Type issues open ea as T x 0 in eb is like leT x 0 2 ea in eb 1cr39eTe values I WhaT is differenT is ThaT eb cannoT know sTaTically whaT The concr39eTe Type of x is so iT cannoT Take advanTage of iT


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

Why people love StudySoup

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

Allison Fischer University of Alabama

"I signed up to be an Elite Notetaker with 2 of my sorority sisters this semester. We just posted our notes weekly and were each making over $600 per month. I LOVE StudySoup!"

Bentley McCaw University of Florida

"I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"


"Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.