{"id":4299,"date":"2019-12-13T14:11:02","date_gmt":"2019-12-13T17:11:02","guid":{"rendered":"http:\/\/www.inf.ufrgs.br\/profcomp\/?page_id=4299"},"modified":"2021-07-01T19:45:27","modified_gmt":"2021-07-01T22:45:27","slug":"cmp194","status":"publish","type":"page","link":"https:\/\/www.inf.ufrgs.br\/profcomp\/lista-de-disciplinas\/cmp194\/","title":{"rendered":"CMP194"},"content":{"rendered":"

Foundations for Rigorous Software Development<\/strong><\/p>\n

Professor<\/strong>: \u00c1lvaro Freitas Moreira
\nPrerequisites<\/strong>: \u2013
\nHours<\/strong>: 60 hs
\nCredits<\/strong>: 4
\nSemesters<\/strong>: First
\nUndergraduate Enrollment<\/strong>: INF05013
\nPage Link<\/strong>: \u2013<\/p>\n

 <\/p>\n

SUMMARY<\/strong><\/p>\n

Lambda Calculus, Simply Typed Lambda Calculus, Polymorphic Types, Dependent Types, Calculus of Constructions, Constructive Interpretation of Propositional and Predicate Logic.<\/p>\n

 <\/p>\n

OBJECTIVES<\/strong><\/p>\n

Programming languages defined on top of formally defined cores together with proof assistants are fundamental tools for rigorous software development. The goals of this course are: (i) to present to the students variations of the lambda calculus, both in the untyped version and in typed versions with simple types and their extensions such as polymorphic and dependent types, (ii) understand the foundations of modern proof assistants like Coq and Agda, as well as (iii) the foundations of modern programming languages such as Haskell, Ocaml, and F#.<\/p>\n

 <\/p>\n

PROGRAM<\/strong><\/p>\n

– Lambda Calculus \u2013 semantics and properties<\/p>\n

– Simply Typed Lambda Calculus \u2013 semantic and properties<\/p>\n

– Constructive Interpretation of Propositional Logic<\/p>\n

– Lambda Calculus with Polymorphic Types \u2013 semantics and properties<\/p>\n

– Lambda Calculus with Dependent Types – semantics and properties<\/p>\n

– Calculus of Constructions \u2013 semantics, and properties<\/p>\n

– Constructive Interpretation of Predicate Logic<\/p>\n

 <\/p>\n

EVALUATION<\/strong><\/p>\n

The evaluation will consist of a number of lists of exercises to be solved individually by the students. The final score M will be given by the arithmetic mean of the scores on the exercises. The final grade can be improved by also taking into account subjective criteria such as class participation and attendance.<\/p>\n

The possible grades are A (score >= 9.0), B (score >= 7.5 and < 9.0), C (score >= 6.0 and < 7.5), D (failed, score< 6.0) or FF (failed, the student attended less than 75% of the classes).<\/p>\n

 <\/p>\n

BIBLIOGRAPHY<\/strong><\/p>\n

    \n
  1. Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof: An Introduction. Cambridge University Press, 2014. ISBN 9781316056349<\/li>\n
  2. Benjamin Pierce. Types and programming languages. Cambridge: MIT Press, 2002. ISBN 0262162091<\/li>\n
  3. Papers on the specific topics discussed will also be recommended<\/li>\n<\/ol>\n

     <\/p>\n","protected":false},"excerpt":{"rendered":"

    Foundations for Rigorous Software Development Professor: \u00c1lvaro Freitas Moreira Prerequisites: \u2013 Hours: 60 hs Credits: 4 Semesters: First Undergraduate Enrollment: INF05013 Page Link: \u2013   SUMMARY Lambda Calculus, Simply Typed Lambda Calculus, Polymorphic Types, Dependent Types, Calculus of Constructions, Constructive Interpretation of Propositional and Predicate Logic.   OBJECTIVES Programming languages defined on top of formally […]<\/p>\n","protected":false},"author":11,"featured_media":0,"parent":462,"menu_order":194,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/4299"}],"collection":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/users\/11"}],"replies":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/comments?post=4299"}],"version-history":[{"count":1,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/4299\/revisions"}],"predecessor-version":[{"id":4300,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/4299\/revisions\/4300"}],"up":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/462"}],"wp:attachment":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/media?parent=4299"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}