Тобиас Нипков - Tobias Nipkow

Тобиас Нипков
Родился1958
ИзвестенИзабель пруф ассистент
Научная карьера
УчрежденияМассачусетский технологический институт, Кембриджский университет, TU Мюнхен
ТезисКонцепции поведенческой реализации недетерминированных типов данных  (1987)
ДокторантКлифф Б. Джонс
Интернет сайтwww21.в.tum.de/ ~ nipkow

Тобиас Нипков (1958 г.р.) - немецкий ученый-компьютерщик.

Карьера

Нипков получил Диплом (MSc) в Информатика от Департамент компьютерных наук из Высшая техническая школа Дармштадта в 1982 г. и его докторская степень. от Манчестерский университет в 1987 г.

Он работал в Массачусетский технологический институт с 1987 г. изменен на Кембриджский университет в 1989 г. и Технический университет Мюнхена в 1992 году, где он был назначен профессором теории программирования.

Он является председателем группы логики и проверки с 2011 года.

Он известен своей работой в области интерактивного и автоматического доказательства теорем, в частности, за Изабель пруф ассистент; он редактор Журнал автоматизированных рассуждений. Кроме того, он специализируется на семантике языков программирования, системах типов и функциональном программировании.[1]

Избранные публикации

  • Мартин У. и Нипков Т. (1986). «Объединение в булевых кольцах». В Jörg H. Siekmann (ed.). Proc. 8-я конференция по автоматическому отчислению. LNCS. 230. Springer. С. 506–513.
  • Тобиас Нипков (1987). Концепции поведенческой реализации недетерминированных типов данных (Кандидатская диссертация). Отчет Департамента компьютерных наук. УМКС-87-5-3. Манчестерский университет.
  • Нипков, Т. (1989). «Комбинирование алгоритмов сопоставления: прямоугольный случай». В Нахум Дершовиц (ред.). Методы перезаписи и приложения, 3-е Int. Конф., РТА-89. LNCS. 355. Springer. С. 343–358.
  • Тобиас Нипков (1990). «Объединение в примальных алгебрах, их степенях и разнообразиях». Журнал ACM. 37 (4): 742–776. Дои:10.1145/96559.96569.
  • Нипков Т. и Цянь З. (1991). «Модульное электронное объединение высшего порядка». В книге Рональд В. (ред.). Методы перезаписи и приложения, 4th Int. Конф., РТА-91. LNCS. 488. Springer. С. 200–214.
  • Тобиас Нипков (1991). «Критические пары высшего порядка». Proc. 6-й симпозиум IEEE по логике в компьютерных науках. С. 342–349.
  • Нипков, Т. (1995). «Системы перезаписи высшего порядка (приглашенная лекция)». В Сян, Цзе (ред.). 6-й Int. Конф. по методам и приложениям перезаписи (RTA). LNCS. 914. Springer. п. 256.
  • Франц Баадер и Тобиас Нипков (1998). Перезапись терминов и все такое. Кембридж: Издательство Кембриджского университета. ISBN  978-0-521-45520-6.
  • Нипков, Тобиас, изд. (1998). Методы перезаписи и приложения, 9-е Int. Конф., РТА-98. LNCS. 1379. Springer.
  • Нипков Т. и Полсон Л. и Венцель М. (2002). Изабель / ХОЛ - помощник по проверке логики высокого порядка. Springer.
  • Гервин Кляйн и Тобиас Нипков (2006). «Машинно-проверенная модель для Java-подобного языка, виртуальной машины и компилятора». Транзакции ACM по языкам и системам программирования. 28 (4): 619–695. Дои:10.1145/1146809.1146811.

использованная литература

  1. ^ Краткая биография

внешние ссылки