Тобиас Нипков
Тобиас Нипков | |
|---|---|
| Рожденный | 1958 |
| Известный | Изабель Пруф помощник |
| Научная карьера | |
| Учреждения | Массачусетский технологический институт , Кембриджский университет , Мюнхенский технический университет |
| Диссертация | Концепции поведенческой реализации недетерминированных типов данных (1987) |
| Докторантура | Клифф Б. Джонс |
| Веб-сайт | www21 |
Тобиас Нипков (1958 г.р.) — немецкий ученый-компьютерщик.
Карьера
[ редактировать ]Нипков получил диплом (магистр) в области компьютерных наук на факультете компьютерных наук Высшей технической школы Дармштадта в 1982 году и докторскую степень. из Манчестерского университета в 1987 году.
С 1987 года он работал в Массачусетском технологическом институте , в 1989 году перешёл в Кембриджский университет , а в 1992 году — в Технический университет Мюнхена , где был назначен профессором теории программирования .
С 2011 года является председателем группы «Логика и верификация».
Он известен своей работой в области интерактивного и автоматического доказательства теорем , в частности, благодаря помощнику по доказательству Изабель ; он был редактором журнала автоматического рассуждения до 1 января 2021 года. [1] Более того, он специализируется на семантике языков программирования , системах типов и функциональном программировании . [2]
В 2021 году он получил премию Эрбрана «в знак признания его лидерства в разработке Isabelle и связанных с ним инструментов, что привело к ключевому вкладу в основы, автоматизацию и использование помощников по проверке в широком спектре приложений, а также за его успешные усилия по увеличению видимость автоматизированного рассуждения». [3]
Избранные публикации
[ редактировать ]- Мартин У. и Нипков Т. (1986). «Объединение в булевых кольцах». В Йорге Х. Зикманне (ред.). Учеб. 8-я конференция по автоматизированному дедукции . ЛНКС . Том. 230. Спрингер. стр. 506–513.
- Тобиас Нипков (1987). Концепции поведенческой реализации недетерминированных типов данных (кандидатская диссертация). Отчет отдела компьютерных наук. Том. УМКС-87-5-3. Университет Манчестера.
- Нипков, Т. (1989). «Комбинирование алгоритмов сопоставления: прямоугольный случай». В Нахуме Дершовице (ред.). Техники и приложения переписывания, 3-й Межд. конф., РТА-89 . ЛНКС. Том. 355. Спрингер. стр. 343–358.
- Тобиас Нипков (1990). «Объединение первичных алгебр, их возможностей и разновидностей» . Журнал АКМ . 37 (4): 742–776. дои : 10.1145/96559.96569 . S2CID 14940917 .
- Нипков Т. и Цянь З. (1991). «Модульная электронная унификация высшего порядка». В книге Рональда В. (ред.). Техники и приложения переписывания, 4-й Межд. конф., РТА-91 . ЛНКС. Том. 488. Спрингер. стр. 200–214.
- Тобиас Нипков (1991). «Критические пары высшего порядка». Учеб. 6-й симпозиум IEEE по логике в информатике . стр. 342–349.
- Нипков, Т. (1995). «Системы перезаписи высшего порядка (приглашенная лекция)». Ин Сян, Цзе (ред.). 6-й Межд. Конф. по методам и приложениям переписывания (RTA) . ЛНКС. Том. 914. Спрингер. п. 256.
- Франц Баадер и Тобиас Нипков (1998). Переписывание терминов и все такое . Кембридж: Издательство Кембриджского университета. ISBN 978-0-521-45520-6 .
- Нипков, Тобиас, изд. (1998). Техники и приложения переписывания, 9-й Межд. конф., РТА-98 . ЛНКС. Том. 1379. Спрингер.
- Нипков Т., Полсон Л. и Венцель М. (2002). Изабель/ХОЛ — Помощник по доказательству логики высшего порядка . Спрингер.
- Гервин Кляйн и Тобиас Нипков (2006). «Машинно-проверенная модель для Java-подобного языка, виртуальной машины и компилятора» . Транзакции ACM в языках и системах программирования . 28 (4): 619–695. дои : 10.1145/1146809.1146811 .
Ссылки
[ редактировать ]- ^ Бланшетт, Жасмин (12 февраля 2021 г.). «Сообщение от нового главного редактора» . Журнал автоматизированного рассуждения . 65 (2): 155. doi : 10.1007/s10817-021-09587-y . hdl : 1871.1/1216cab9-08c1-4d41-8069-aa1735f5786d .
- ^ Краткая биография
- ^ «Премия Эрбрана за выдающийся вклад в автоматизированное мышление» . КЕЙД Инк . Проверено 14 июля 2021 г.
Внешние ссылки
[ редактировать ]| Международный | |
|---|---|
| Национальный | |
| академики | |
| Другой | |
