Мадс Тофте
Мадс Тофте | |
|---|---|
| Рожденный | 20 апреля 1959 г. Люнгбю, Дания |
| Гражданство | датский |
| Образование | Копенгагенский университет ( магистр ) Эдинбургский университет ( доктор философии ) |
| Известный | Стандартный ML ИТ-университет Копенгагена |
| Награды | ИТ-премия 2002 г. |
| Научная карьера | |
| Поля | Информатика |
| Учреждения | Копенгагенский университет Эдинбургский университет Университет Нигерии ИТ-университет Копенгагена |
| Тезис | Операционная семантика и вывод полиморфного типа (1987) |
| Докторантура | Робин Милнер |
| Веб-сайт | www |
Мадс Тофте (родился 20 апреля 1959 г.) — датский ученый-компьютерщик , внесший, в частности, вклад в функциональное программирование и Standard ML язык программирования .
Образование [ править ]
Тофте родился в Люнгбю , Дания, и вырос в Хольбеке , Дания . Он изучал информатику и математику в Копенгагенском университете , где получил степень магистра (под руководством Нила Д. Джонса ) в 1984 году; затем в Эдинбургском университете , где он получил степень доктора философии в 1988 году (под руководством Робина Милнера ). Он является почетным доктором Кингстонского университета в 2007 году .
и карьера Исследования
В своей магистерской диссертации 1984 г. [1] и в предыдущей работе он исследовал и формализовал генератор компилятора CERES (совместно с Нилом Д. Джонсом) и показал, что (1) генератор компилятора сам по себе является компилятором определений языка в компиляторы; и (2) при подходящих предположениях существует определение языка, которое при применении к самому себе генерирует генератор компилятора. Это тесно связано с самостоятельным применением при частичной оценке .
В своей докторской диссертации он разработал и доказал правильность первой системы звуковых типов для ML в стиле полиморфных ссылок , что в то время было важной открытой проблемой. Более того, он формализовал вариант модульной системы языка программирования Standard ML .
Мадс Тофте — соавтор «Определения». [2] Standard ML и связанный с ним комментарий, вероятно, наиболее точное описание, разработанное для любого реалистичного языка программирования. Он был соавтором ML Kit — реализации Standard ML , структура которой точно соответствует определению.
Впоследствии он разработал (совместно с Жан-Пьером Тальпеном ) понятие вывода регионов — методику анализа программ и управления памятью , позволяющую избежать или свести к минимуму использование сборки мусора . Эта работа была впервые опубликована [3] в POPL 1994, а в 2005 году он получил награду Ассоциации вычислительной техники (ACM) POPL 1994 за самую влиятельную бумагу.
разработал В конце девяностых он совместно с Фрицем Хенглейном и другими систему типов и сложный инструмент под названием AnnoDomini для смягчения последствий в Проблема 2000 года программном обеспечении COBOL . Инструмент анализирует устаревшие программы, чтобы обнаружить все поля данных, которые используются в качестве дат. Этот Работа была представлена в рамках приглашенного доклада POPL 1999 года. [4]
В апреле 1999 года он был назначен первым управляющим директором Копенгагенского университета информационных технологий . Он курировал создание университета с нуля, найм преподавателей/персонала, набор студентов и разработку учебных программ. Первые студенты появились спустя 5 месяцев, в сентябре 1999 года. С 2003 года он является вице-канцлером ИТ -университета Копенгагена .
В апреле 2018 года было объявлено, что он покинет Копенгагенский ИТ-университет в конце года. В январе 2019 года он объявил, что уезжает из Дании, чтобы быть со своей дочерью, из-за иммиграционного законодательства Дании, которое не позволяет ей въехать в страну. [5]
Награды [ править ]
- 2002 Премия IDG IT ( IT-prisen ) за лидерство в ИТ-университете Копенгагена.
- 2005 Премия ACM POPL '94 за самую влиятельную бумагу (совместно с Жан-Пьером Тальпеном).
Ссылки [ править ]
- ^ М. Тофте: Генераторы-компиляторы: что они могут делать, что они могут делать и чего они, вероятно, никогда не будут делать. Спрингер-Верлаг 1990 г.
- ^ Р. Милнер , М. Тофте, Р. Харпер : Определение стандарта ML, MIT Press 1990, второе издание 1997 г.
- ^ М. Тофте и Ж.-П. Талпин: реализация типизированного лямбда-исчисления с вызовом по значению с использованием стека регионов , в материалах POPL, 1994 г.
- ^ PH Эйдорф, Ф. Хенглейн, К. Моссин, Х. Нисс, М. Х. Соренсен, М. Тофте: AnnoDomini: От теории типов к инструменту преобразования 2000 года . В материалах ПОПЛ 1999 г.
- ^ Тофте, Мэдс. «Сейчас я покидаю Данию в знак протеста против крайних правил, которые не позволяют моей приемной дочери из Африки приехать в страну» . Политика . Проверено 28 января 2019 г.
Внешние ссылки [ править ]
| Международный | |
|---|---|
| Национальный | |
| академики | |
| Другой | |
