Tobias Nipkow (nacido en 1958) es un informático alemán.
Tobias Nipkow | |
---|---|
Nació | 1958 |
Conocido por | Asistente de pruebas de Isabelle |
Carrera científica | |
Instituciones | MIT , Universidad de Cambridge , TU Munich |
Tesis | Conceptos de implementación de comportamiento para tipos de datos no deterministas (1987) |
Asesor de doctorado | Cliff B. Jones |
Sitio web | www21 |
Carrera profesional
Nipkow recibió su Diplom (MSc) en Ciencias de la Computación del Departamento de Ciencias de la Computación de la Technische Hochschule Darmstadt en 1982, y su Ph.D. de la Universidad de Manchester en 1987.
Trabajó en el MIT desde 1987, se mudó a la Universidad de Cambridge en 1989 y a la Universidad Técnica de Múnich en 1992, donde fue nombrado profesor de teoría de la programación.
Es presidente del grupo de Lógica y Verificación desde 2011.
Es conocido por su trabajo en la demostración automática e interactiva de teoremas, en particular por el asistente de pruebas de Isabelle ; es el editor del Journal of Automated Reasoning . Además, se centra en la semántica de los lenguajes de programación, los sistemas de tipos y la programación funcional. [1]
Publicaciones Seleccionadas
- Martin, U. y Nipkow, T. (1986). "Unificación en anillos booleanos". En Jörg H. Siekmann (ed.). Proc. VIII Jornadas de Deducción Automatizada . LNCS . 230 . Saltador. págs. 506–513.
- Tobias Nipkow (1987). Conceptos de implementación de comportamiento para tipos de datos no deterministas (tesis doctoral). Informe del Departamento de Ciencias de la Computación. UMCS-87-5-3. Universidad de Manchester.
- Nipkow, T. (1989). "Combinando algoritmos coincidentes: el caso rectangular". En Nachum Dershowitz (ed.). Técnicas y aplicaciones de reescritura, 3rd Int. Conf., RTA-89 . LNCS. 355 . Saltador. págs. 343–358.
- Tobias Nipkow (1990). "Unificación en álgebras primarias, sus poderes y sus variedades". Revista de la ACM . 37 (4): 742–776. doi : 10.1145 / 96559.96569 . S2CID 14940917 .
- Nipkow, T. y Qian, Z. (1991). "E-Unificación modular de orden superior". En Libro, Ronald V. (ed.). Técnicas y aplicaciones de reescritura, 4ª Int. Conf., RTA-91 . LNCS. 488 . Saltador. págs. 200–214.
- Tobias Nipkow (1991). "Pares críticos de orden superior". Proc. 6º Simposio IEEE sobre Lógica en Ciencias de la Computación . págs. 342–349.
- Nipkow, T. (1995). "Sistemas de reescritura de orden superior (conferencia invitada)". En Hsiang, Jieh (ed.). 6ta Int. Conf. sobre técnicas y aplicaciones de reescritura (RTA) . LNCS. 914 . Saltador. pag. 256.
- Franz Baader y Tobias Nipkow (1998). Reescritura de términos y todo eso . Cambridge: Cambridge University Press. ISBN 978-0-521-45520-6.
- Nipkow, Tobias, ed. (1998). Técnicas y aplicaciones de reescritura, 9º Int. Conf., RTA-98 . LNCS. 1379 . Saltador.
- Nipkow T. y Paulson L. y Wenzel M. (2002). Isabelle / HOL - Asistente de pruebas para lógica de orden superior . Saltador.
- Gerwin Klein y Tobias Nipkow (2006). "Un modelo comprobado por máquina para un compilador, máquina virtual y lenguaje similar a Java" . Transacciones ACM sobre lenguajes y sistemas de programación . 28 (4): 619–695. doi : 10.1145 / 1146809.1146811 .