Course OverviewAdministrative StuffThe Coq Proof AssistantCIS 500Software FoundationsSpring 2011Lecture 1Course OverviewWhat is “software foundations”?Software foundations (or “theory of programming languages”) isthe mathematical study of the meaning of programs.The goal is finding ways to describe program behaviors that areboth precise and abstract.•precise so that we can use mathematical tools to formalizeand check interesting properties•abstract so that properties of interest can be discussedclearly, without getting bogged down in low-level detailsWhy study software foundations?•To prove spec ific properties of particular programs (i.e.,program verification)•Important in some domains (safety-critical systems, hardwaredesign, security protocols, inner loops of key algorithms, ...),but still fairly difficult and expensive•To develop intuitions for informal reasoning about programs•To prove general facts about all the programs in a givenprogramming language (e.g., safety or isolation properties)•To deeply understand language features (and theirinteractions) and develop principles for better language design(PL is the “materials science” of computer science...)Questions This Course Could Help Answer•“I’m designing a new web scripting language that’s going totake over the world. How can I specify it so that differentpeople implementing compilers will know how it is supposedto behave?”•I’m writing a compiler and I’d like to add this optimization,but I’m not convinced it’s always correct. How can I be sure?”•“I want to write a program analysis tool that examines PERLprograms and checks for possible command injection attacks.How can I know I haven’t missed any?”Approaches to Program Meaning•Denotational semantics and domain theory view programs as simplemathematical objects, abstracting away their flow of control andconcentrating on their input-output b e havior.•Program logics such as Hoare logic and dependent type theoriesfocus on logical rules for reasoning about programs.•Operational semantics describes program behaviors by means ofabstract machines. This approach is somewhat lower-level than theothers, but is extremely flexible.•Process calculi focus on the communication and synchronizationbehaviors of complex concurrent systems.•Type systems describe approximations of program behaviors,concentrating on the shapes of the values passed between differentparts of the program.OverviewWe will concentrate on operational techniques and type systems.1. Part I: Foundations1.1 Functional programming1.2 Inductive definitions and proof techniques1.3 Constructive logic1.4 The Coq proof assistant2. Basics2.1 Reasoning about simple imperative programs2.2 Operational semantics3. Type systems3.1 Simply typed lambda-calculus3.2 Type safety3.3 SubtypingWhat you’ll get out of the course•A more sophisticated perspective on programs, programminglanguages, and the activity of programming•How to view programs and whole languages as formal,mathematical objects•How to make and prove rigorous claims about them•Detailed study of a range of basic language features•Powerful mathematical tools for language (and software)design, description, and analysis•Constructive logic•Inductive methods of definition and proof•Expertise using a cutting-edge mechanical proof assistantMost software designers are language designers, at some point!What this course is not•An introduction to programming (see CIT 591)•A course on functional programming (though we’ll be doingsome functional programming along the way)•A course on compilers (you should ideally already have basicconcepts such as lexical analysis, parsing, abstract syntax, andscope under your belt)•A comparative survey of many different programminglanguages and styles (boring!)Administrative StuffPersonnelInstructor: Benjamin PierceLevine 562Teaching Assistants: Anthony CowleyBrent YorgeyAdministrative Assistant: Marissa MeleLevine 311InformationTextbook: Software Foundations(see web page)Webpage: http://www.seas.upenn.edu/∼cis500Mailing list:[email protected]•Two in-class midterms•Wednesday, Feb 16•Wednesday, Mar 30•Final exam•Date not yet announcedGradingFinal course grades will be computed as follows:•Homework: 20%•2 midterms: 20% each•Final: 40%(Lack of) extra Credit1. Grade improvements can only be obtained by sitting in on thecourse next year and turning in all homeworks and exams.(If you are doing this to improve your grade from last year,please speak to me after class so I know who you are.)2. There will be no extra credit projects, either during thesemester or after the course ends. Concentrate your efforts onthis course, now.Collaboration•Collaboration on homework is strongly encouraged•Studying with other people is the best way to internalize thematerial•Form study groups!•2 people is the ideal size.•3 is OK.•4 is too many.“You never really misunderstand somethinguntil you try to teach it...”— Anon.Homework•Small part of your grade, but a large part of yourunderstanding — impossible to perform well on examswithout seriously grappling with the homework•Submit one assignment per study group•On written parts of homeworks, we will grade a semi-randomsubset of the problems on each assignment•Late policy: Late homeworks lose 25% of their value for eachday (or partial day) after the announced deadlineFirst Homework Assignment•The first homework assignment is due next Wednesday by3PM.•You will need:•An account on a machine where Coq is installed (you can alsoinstall Coq on your own machine if you like)•Instructions on running Coq (available on the course web page)•The files Preface.v and Basics.v from the course web pageNo Class MondayNext Monday is Martin Luther King day.Instead of coming to class, go out and do some thing for yourcommunity.Office Hours•Office hours will be held in the linux lab so that people can sitand work on their homework with a TA nearby, if they wish.The WPE-I•PhD students in CIS must pass a five-section WrittenPreliminary Exam (WPE-I)Software Foundations is one of the five areas•The final for this course is also the software foundationsWPE-I exam•Near the end of the semester, you will be given an opportunityto declare your intention to take the final exam for WPE creditThe WPE-I (continued)•You do not need to be enrolled in the c ourse to take the examfor WPE