Beskjeder

Dear all,

You should all have gotten feedback to home exam 2. Also you should have received a plan for the oral exam.

If any of you are missing some of this information, please, write to me.

Best,
Michael

Just to ensure, there will not be any exercises today. 

Dear all,

We would like to get your input to the course. We have therefore created a Netskjema for a course evaluation. You should all have gotten an invitation to this.

Best,
Michael

Dear all,

You can not find the oral exam description and questions on the site:

/studier/emner/matnat/ifi/IN5630/v24/exam/

You have the chance to ask question to this on Wednesday. 

We will make the plan for the oral exam just after the hand-in of final homework. But all that previously have written about restrictions will get either the early or the late date mentioned in their specific communication.

Dear all,

We are all coming to the end of the course and next week will be the final one. The plan is as follows.

Tuesday 21.
Deadline for Home exam 2. Inspera should be open now

Wednesday 22.

• Q/A. You can here ask about the course and the exam. We will Monday post the exam questions and how the exam will be conducted. Next week we will also fix the schedule for the exam.
• Guest lecture: Tobias Reinhard will give an introduction to seperation logic.

You are all invited to this guest lecture.

Title: Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs
Speaker: Tobias Reinhard, TU Darmstadt, Germany
Time: Tue 21 May @ 11:05
Place: Seminarrom Perl

Abstract:
We present the first study of completeness thresholds (CTs) for infinite state systems.
Any bounded proof reaching its CT is sound. Thereby, CTs allow us to reduce unbounded proofs to bounded ones.
Specifically, we focus on memory safety proofs for programs that iterate over arbitrarily large data structures in a memory-layout-preserving way. Meanwhile, many of the results straightforwardly apply to arbitrary correctness properties.
We present a generic approach to extract CTs from a program's verification condition and show that it scales. Moreover, we demonstrate that we can characterise CTs for interesting classes of array traversing programs.
 

Hello students!

Sorry for the late message. But just to avoid any confusion; given that the deadline for Home Exam 2 is approaching, today will be another Q&A session. Feel free to work on some of the exercises from the previous weeks if you please --- you can ask questions about those as well.

See you at 10:15!

Dear all,

Due to May 1st there is not lecture this week. 

However, on Thursday Lars will still be at the exercises and can help you with the home exam and other questions you may have.

Note, that next week Joachim with lecture on type inference and implementation in Haskell. However, there will be no exercises next week due to Ascension Day.

Dear all,

The deadline for home exam 2 have been pushed until Tuesday Maj 21.

Now you have time to do a very good job. :)

Michael

Following the guest lecture Wednesday there will be no exercises. Instead there is be a talk (Thu from 10:15 in Java; where we have exercises). The talk will be

Title: Perspectives of Semantic Modeling in Categories
Speaker: William Steingartner, assoc. prof., PhD.,
Techical University of Kosice, Slovakia

The talk will be much related to the material of the course, but take it to the next level.

Abstract:
The reliability of programs and program systems is a very topical issue, especially due to the rapidly evolving technologies present in all areas of daily life. Different approaches are used to achieve reliability in the development of programs and program systems. All these techniques are based on formal models of system functionality and these models are grounded in the formal semantics of the programming languages used.

In this talk, we show the most importan...

Hei all,

Next week will be slightly different.

On Wednesday Jan Perhac from the Technical University of Kosice will give the lecture, that will be on

Introduction to Type inference and Let polymorphism

Though this is a guest lecture, the following week we will implement a type system in Haskell, where type inference and polymorphism is very central. The reading material also relates to this.

Hi all,

You can find the home exam 2 here: Home exam 2

You should all also have received a grade and feedback for the first home exam. You might have to request feedback to get the feedback.

You are welcome to ask Lars about both tomorrow at the exercises.

Dear all,

We are planing that the oral exam on the course will be in the week of Jun 3 to Jun 7. The day(s) is(are) not fixed yet. We likely have to spread it over two days that week.

I know that it is early, but if you already now know about any other exam conflicts, then write to me.

Best,
Michael

Hello students,

The exercises for tomorrow have been published here.

Further, my plan is to go over the overall strategies for implementing the interpreter from Oblig 1. Note that we will not discuss any actual implementations, but rather an overall approach for some of the more challenging parts.

See you tomorrow!

We have updated the assignment text for part 2 of the first Home Exam (the Boa miniproject). The updated assignment text can be found here.

Happy Coding.

- The teaching team.

 

On the course we will as mentioned have one optional assignment, that give you the option to get some feedback, and two home exams. All individual. 

The deadlines for all are:

• Optional assignment: Feb 29 - This is Boa part 1, we have moved this a bit, as we can understand that there have been some confusions. 
• Home exam 1: Mar 22 - Boa part 2; this is an extension to Boa part 1
• Home exam 2: May 3

We follow the normal rules for extensions: small extension for assignments and strict deadline for home exams.

About the optional assignment, you are much welcome (and even encouraged) to write a page about your thoughts. What choices have you made and why? That will give Lars the possibility to give you better feedback.

About Home Exam 1, then it seems that the text is not complete and Joachim have will update this.

After yesterdays exercises I have made a basic parser framework with way too many comments.

There is however still some holes for parsing the exact expressions. 

Please consult the Parsec documentation for further details and inspiration. Look especially at `chainl` and `chainr` combinators

https://hackage.haskell.org/package/parsec-3.1.17.0/docs/Text-ParserCombinators-Parsec.html

In order to make the assignment texts easier to find, we have created a folder called Assignments. We have moved all files regarding the Boa Interpreter there.

Kind regards, The Teaching Team

The course will have two home-exam that will each count 25 % of the grade.

To help you get started we first will post an optional assignment. That will give you the option to get feedback before the forst home-exam.

The content of this assignment will be overlapping with the first home-exam. It will be posted in a couple of weeks.

More information will be posted here: 

https://github.uio.no/IN5630/v24/blob/main/README.md#exam

There was a question about location of material for the course. 

Specifically we will not use Canvas. Material vil be posted here and on the UiO-github repository; linket below.

There was a question about location of material for the course. 

Specifically we will not use Canvas. Material vil be posted here and on the UiO-github repository; linket below.

There was a question about location of material for the course. 

Specifically we will not use Canvas. Material vil be posted here and on the UiO-github repository; linket below.

We look much forward to seeing you on the course and teach you how we can implement programming langauge and gain deeper understanding by formalising them.