?

Log in

Дневник одного математика ;)
 
[Most Recent Entries] [Calendar View] [Friends]

Below are the 8 most recent journal entries recorded in Dmytro Mitin's LiveJournal:

Monday, May 22nd, 2017
4:02 pm
Habrahabr
My post in Habrahabr blog (in Russian)
https://habrahabr.ru/post/329176/
From dependent types to Homotopy type theory in Scala + Shapeless + ProvingGround

#scala
Wednesday, May 3rd, 2017
10:21 pm
Interview with Albert
Albert

Hello Albert. You are one of the most active learners in my course «Introduction to programming with dependent types in Scala». Would you agree to give an interview to me?

Hi Dmytro,
I'd love to do the interview as I'm grateful for your kindly help on the type level programming lesson.
I've took quite a few MOOCs online, but none of the teachers spent so much effort on answering student's questions in such a timely manner. It feels like enjoying a private lesson, so as to speak I owe you a favour for this wonderful lesson.
It is perhaps some what related to the nature of this course, it is abstract and not easily followed. So right now not so many people are actively participating in it. Otherwise you'd be busy around all day long to answer all student's question.

Back to the lesson, I haven't felt I learned «type level programming». But now I know what «type level programming» is, what an automated proof is. It is fun to go through all lessons and fill in the blanks in the exercise. I might still have a lot to learn to truly understand and use it appropriately in my daily work.

I sincerely hope people like me who know a little functional programming and want to dig into this could enjoy this course as well.

Thank you for your warm words.
So let's start our interview.
Would you tell us several words about yourself?


Continue...Collapse )
Friday, March 31st, 2017
11:47 pm
Introduction to programming with dependent types in Scala
All videos are online. Totally 8 hours of video, 130 slides, and 50 programming exercises (in pure Scala and in Scala + ProvingGround library).
https://stepik.org/2294
1 Theory
1.1 Installing software https://goo.gl/ZmIdzy
1.2 Dependent types https://goo.gl/6AhLf7
1.3 Path-dependent types https://goo.gl/bWgUCr
1.4 Type classes https://goo.gl/zqx1ra
1.5 Product type https://goo.gl/KAdaSD
1.6 Co-product type (sum type) https://goo.gl/qogGSF
1.7 Function type https://goo.gl/j1fRio
1.8 Dependent pair type (Σ-type) https://goo.gl/h8cmDG
1.9 Dependent function type (Π-type) https://goo.gl/6hGcq3
1.10 Empty and unit types https://goo.gl/e9JTD7
1.11 Boolean type https://goo.gl/vlR833
1.12 Type of natural numbers https://goo.gl/lBnbh8
1.13 List type https://goo.gl/H64rOg
1.14 Type of fixed-length vectors https://goo.gl/9p5KwO
1.15 Identity type. Curry–Howard correspondence https://goo.gl/15EDMw
1.16 Eliminators into dependent types (induction) https://goo.gl/C2Mrd7
1.17 Type-level programming https://goo.gl/5XPk4K
2 Practice
Thursday, March 23rd, 2017
2:12 pm
Introduction to programming with dependent types in Scala
https://stepik.org/course/ThCS-Introduction-to-programming-with-dependent-types-in-Scala-2294/

This course is an introduction to type theory, homotopy type theory (HoTT), dependent-type programming, type-level programming, and theorem proving using Scala.

Till 31 March the course is in beta. Slides and exercices are mostly ready, some videos will be added soon.
Wednesday, November 25th, 2009
5:33 pm
Интервью
По приколу дал интервью студентам для мехматовской газеты:

страница 1

страница 2
Tuesday, July 8th, 2008
8:37 pm
Попиарим научный форум dxdy.ru

Буду благодарен, если попиарите форум среди знакомых.

Приглашаю посетить научный форум dxdy.ru. Более 100'000 сообщений, более 10'000 пользователей, около 15'000 тем по



Кроме высококвалифицированных участников форум от аналогов отличает давно и успешно реализованная возможность оформлять математические формулы в нотации \LaTeX. Например, в теме Проверка на простоту без такого наглядного и всемирно используемого инструмента просто не обойтись.

В общем, добро пожаловать! Помните, что за вас задачи у нас не решают, у нас помогут решить и разобраться, но основную работу должны проделать вы сами.


Если будете размещать у себя эту рекламку, то вот удобное окошко, чтобы скопипастить html-код:


Спасибо!

(c) cepesh
Tuesday, March 18th, 2008
5:18 pm
Sunday, January 6th, 2008
12:05 am
About LiveJournal.com