DOC PREVIEW
Penn CIS 500 - CIS500 Software Foundations - Course Overview

This preview shows page 1-2-3-4-5 out of 15 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

CIS 500Software FoundationsFall 2006September 6Course 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.Iprecise so that we can use mathematical tools to formalizeand check interesting propertiesIabstract so that properties of interest can be discussed clearly,without getting bogged down in low-level detailsWhy study software foundations?ITo prove specific properties of particular programs (i.e.,program verification)IImportant in some domains (safety-critical systems, hardwaredesign, security protocols, inner loops of key algorithms, ...),but still quite difficult and expensiveITo develop intuitions for informal reasoning about programsITo prove general facts about all the programs in a givenprogramming language (e.g., safety or isolation properties)ITo understand language features (and their interactions)deeply and develop principles for better language design(PL is the “materials sc ience ” of computer science...)What you can expect to get out of the courseIA more sophisticated perspective on programs, programminglanguages, and the activity of programmingIHow to view programs and whole languages as formal,mathematical objectsIHow to make and prove rigorous claims about themIDetailed study of a range of basic language featuresIDeep intuitions about key language properties such as typesafetyIPowerful tools for language design, description, and analysisMost software designers are language designers!What this course is notIAn introduction to programming (see CIT 591)IA course on functional programming (though we’ll be doingsome functional programming along the way)IA course on compilers (you should already have basicconcepts such as lexical analysis, parsing, abstract syntax, andscope under your belt)IA comparative survey of many different programminglanguages and styles (boring!)IA seminar on programming language research (see CIS700/002 MW 1:30-3:00, Towne 307)Approaches to Program MeaningIDenotational semantics and domain theory view programs as simplemathematical objects, abstracting away their flow of control andconcentrating on their input-output behavior.IProgram logics such as Hoare logic and dependent type theoriesfocus on logical rules for reasoning about programs.IOperational semantics describes program behaviors by means ofabstract machines. This approach is somewhat lower-level than theothers, but is extremely flexible.IProcess calculi focus on the communication and synchronizationbehaviors of complex concurrent systems.IType systems describe approximations of program behaviors,concentrating on the shapes of the values passed between differentparts of the program.OverviewIn this course, we will concentrate on operational techniques andtype systems.IPart O: Functional ProgrammingIA taste of OCamlIFunctional programming styleIImplementing programming languagesIPart I: Modelling programming languagesISyntax and operational semanticsIInductive proof techniquesIThe lambda-calculusISyntactic sugar; fully abstract translationsOverviewIPart II: Type sys tem sISimple typesIType safetyIReferencesISubtypingIPart III: Object-oriented features (case study)IA simple imperative object modelIAn analysis of core JavaAdministrative StuffPersonnelInstructor: Benjamin PierceLevine [email protected] hours: Wed, 3:00–5:00(subject to change!)Teaching Assistant: Brian AydemirAdministrative Assistant: Kamila Dyjas MauroInformationTextbook: Types and Programming Languages,Benjamin C. Pierce, MIT Press, 2002Webpage: http://www.seas.upenn.edu/∼cis500Mailing list: To be announcedExams1. First mid-term: Wednesday, October 13, in class2. Second mid-term: Wednesday, November 10, in class3. Final: Wednesday, December 20, 9–11AMGradingFinal course grades will be computed as follows:IHomework: 20%I2 midterms: 20% eachIFinal: 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.CollaborationICollaboration on homework is strongly encouragedIStudying with other people is the best way to internalize thematerialIForm study groups!2-3 people is a good size. 4 is too many for all to have equalinput.“You never really misunderstand somethinguntil you try to teach it...”— Anon.HomeworkReadings from TAPL...IShould be completed before lecture (see course web page)IDo all one star questions while reading (no need to turn in)IWrite down questions to ask in class or recitationHomeworkWritten homework...ISmall part of your grade, but a large part of yourunderstandingISubmit one assignment per study group.IWe will grade a semi-random subset of the problems on eachassignmentISome solutions are in the back of the book. Write youranswer down before lookingILate (non-)policy: Homework will not b e accepted after theannounced deadlineFirst Homework AssignmentIThe first homework assignment (on basic OCamlprogramming) is due next Monday by noon.IYou will need:IAn account on a machine where OCaml is installed (you canalso install OCaml on your own machine if you like)IJason Hickey’s notes on OCaml (read chapters 1-5)RecitationsIThere will be both “review” and “advanced” recitationsIRecitations will start next week; they will take place onThursdays or FridaysIThe exact schedule will be organized in the next couple of daysThe WPE-IIPhD students in CIS must pass a five-section WrittenPreliminary Exam (WPE-I)Software Foundations is one of the five areasIThe final for this course is also the software foundationsWPE-I examINear 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)IYou do not need to be enrolled in the course to take the examfor WPE creditIIf you are enrolled in the course and also take the exam forWPE credit, you will receive two grades: a letter grade for thecourse final and a Pass/Fail for the WPEIYou may take the exam for WPE credit even if you are notcurrently enrolled in the PhD programThe WPE-I syllabusIReading knowledge of core OCamlIChapters 1-11


View Full Document

Penn CIS 500 - CIS500 Software Foundations - Course Overview

Download CIS500 Software Foundations - Course Overview
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view CIS500 Software Foundations - Course Overview and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view CIS500 Software Foundations - Course Overview 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?