Man

ERIC TANTER

Profesor Titular

UNIVERSIDAD DE CHILE - DEPTO DE CIENCIAS DE LA COMPUTACION

Santiago, Chile

Líneas de Investigación


Programming Languages; Program Verification; Software Engineering

Educación

  •  Computer Science, UNIVERSIDAD DE CHILE. Chile, 2004
  •  Computer Science, UNIVERSITE DE NANTES. Francia, 2004
  •  Computer Science, VRIJE UNIVERSITEIT BRUSSEL. Bélgica, 2000
  •  Engineer in Computer Systems, ECOLE DES MINES DE NANTES. Francia, 2000

Experiencia Académica

  •   Profesor Titular Full Time

    UNIVERSIDAD DE CHILE

    FCFM

    Santiago, Chile

    2014 - A la fecha

  •   Profesor Asociado Full Time

    UNIVERSIDAD DE CHILE

    FCFM

    Santiago, Chile

    2010 - 2014

  •   Profesor Asistente Full Time

    UNIVERSIDAD DE CHILE

    FCFM

    Santiago, Chile

    2006 - 2010

Formación de Capital Humano


Currently supervising 3 PhD students:
- Elizabeth Labrada. To be defended in 2021/early 2022.
- Stefan Malewski. Started 2020.
- Bruno García Agapito da Veiga. Started 2021.

Currently supervising 1 MSc student:
- Damian Arquez [co-advised with Matías Toro]. To be defended in 2021.

Currently closely involved in the co-supervision of PhD students abroad:
- Joseph Eremondi, University of British Columbia, Canada, with Prof. Ronald Garcia
- Meven Bertrand, Inria Rennes, with Dr. Nicolas Tabareau
- Jenna Wise, Carnegie Mellon University, USA, with Jonathan Aldrich

Graduated 9 PhD students:
- Raimil Cruz: Type Abstraction and Faceted Types for Declassification. Defended 15/01/2020.
- Matías Toro: Abstracting Gradual Typing: Metatheory and Applications. Defended 05/07/2019.
- Oscar Callaú: Empirically-Driven Design and Implementation of Gradualtalk. [co-advised with Romain Robbes]. Defended 27/01/2015.
- Esteban Allende: Improving the Efficiency and Reliability of Gradual Typing [co-advised with Johan Fabry]. Defended 08/01/2015.
- Rodolfo Toledo: Modular and Secure Access Control with Aspects. Defended 13/05/2014.
- Ismael Figueroa: Effective Aspects: A Typed Monadic Model to Control and Reason About Aspect Interference [co-advised with Nicolas Tabareau]. Defended 22/04/2014.
- Christophe Scholliers: Ambient Contracts (Vrije Universiteit Brussel) [co-advised with Wolfgang De Meuter]. Defended 07/02/2013.
- Paul Leger: Opening Up Trace-Based Mechanisms. Defended 05/10/2012.
- Guillaume Pothier: Towards Practical Omniscient Debugging. Defended 13/06/2011.

Graduated 9 MSc students:
- Hans Fehrmann: A Reasonably Exceptional Type Theory [co-advised with Nicolas Tabareau]. Defended 29/12/2020.
- Fabian Mosso: Countable Polymorphic May-Must Effects [co-advised with Matías Toro]. Defended 12/06/2020.
- Nicolás Lehmann: Gradual Refinement Types. Defended 9/3/2017.
- Johannes Bader: Gradual Program Verification with Implicit Dynamic Frames (Karlsruhe Institute of Technology) [co-advised with Jonathan Aldrich (CMU) and Gregor Snelting (KIT)]. Defended 4/10/2016.
- Gustavo Soto: Modular Composition of Session Types. Defended 1/12/2015.
- Matías Toro: Customizable Gradual Effects for Scala. Defended 18/05/2015.
- Felipe Bañados: Gradual Typing for Generic Type-and-Effect Systems [co-advised with Ron Garcia]. Defended 08/08/2014.
- Milton Inostroza: Safe and Practical Decoupling of Aspects with Join Point Interfaces [co-advised with Eric Bodden]. Defended 12/04/2013.
- Victor Ramiro: An Open Proximity Model for Service Discovery in Pervasive Computing. Defended 2009.


Difusión y Transferencia


Awards from industrial partners:
- In 2015 and 2016, I was awarded a Google Faculty Research Award, for working on the principles of gradual security typing for the Web, together with my PhD student Raimil Cruz.
- With Jonathan Aldrich's group at Carnegie Mellon University, I was awarded a Facebook Research Testing and Verification Award in 2018, for developing the principles and applications of gradual verification.
Both awards had high media coverage globally, giving visibility to the areas of gradual typing and incremental program verification.


Premios y Distinciones

  •   Testing and Verification Award

    Facebook Research

    Estados Unidos, 2018

    Incremental Verification, Gradually

  •   Faculty Research Award

    Google

    Estados Unidos, 2015

    Gradual Security Typing for the Web

  •   Faculty Research Award

    Google

    Estados Unidos, 2016

    Gradual Security Typing for the Web


 

Article (65)

The Marriage of Univalence and Parametricity
Abstracting Gradual References
Gradual Verification of Recursive Heap Data Structures
A Reasonably Exceptional Type Theory
Approximate Normalization for Gradual Dependent Types
Chemical foundations of distributed aspects
Dijkstra Monads for All
Gradual Parametricity, Revisited
Chemical Foundations of Distributed Aspects
Foundations of Dependent Interoperability
Gradual Liquid Type Inference
Gradual program verification
Effect capabilities for Haskell: Taming effect interference in monadic programming
Gradual Certified Programming in Coq
Polymorphic bytecode instrumentation
A Taxonomy of Domain-Specific Aspect Languages
An expressive stateful aspect language
Computational contracts
Customizable Gradual Polymorphic Effects for Scala
Object-oriented software extensions in practice
On the Use of Type Predicates in Object-Oriented Software: The Case of Smalltalk
A Theory of Gradual Effect Systems
An empirical study on the impact of static typing on software maintainability
Cast Insertion Strategies for Gradually-Typed Objects
Confined Gradual Typing
ECOCAM, A CONTEXT SENSITIVE COMPUTATIONAL SYSTEM TO PROMOTE MENTAL CALCULATION STRATEGIES: DESIGN CHARACTERISTICS AND PRELIMINARY RESULTS
ECOCAM, A CONTEXT SENSITIVE COMPUTATIONAL SYSTEM TO PROMOTE MENTAL CALCULATION STRATEGIES: DESIGN CHARACTERISTICS AND PRELIMINARY RESULTS
ECOCAM, a context sensitive computational system to promote mental calculation strategies: Design characteristics and preliminary results [ECOCAM, un sistema computacional adaptable al contexto para promover estrategias de cálculo mental: Características de su diseño y resultados preliminares]
Execution Levels for Aspect-Oriented Programming: Design, Semantics, Implementations and Applications
Foundations of Typestate-Oriented Programming
Gradual typing for Smalltalk
Join Point Interfaces for Safe and Flexible Decoupling of Aspects
Parallel actor monitors: Disentangling task-level parallelism from data partitioning in the actor model
How (and why) developers use the dynamic features of programming languages: the case of smalltalk
Modular and flexible causality control on the Web
Programming with Ghosts
Aspectizing Java Access Control
Access Control in JavaScript
Ambient contracts: verifying and enforcing ambient object compositions A la carte
COGNITIVE STRATEGIES FOR MENTAL CALCULATION
Composition of Dynamic Analysis Aspects
First-Class State Change in Plaid
Scoping strategies for distributed aspects
Back to the Future: Omniscient Debugging
Beyond Static and Dynamic Scope
Infrastructure for domain-specific aspect languages: the ReLAx case study
Mirror-based reflection in AmbientTalk
Supporting Composition of Structural Aspects in an AOP Kernel
A Lightweight and Extensible AspectJ Implementation
Controlling Aspect Reentrancy
Flexible metaprogramming and AOP in Java
KALA: Kernel aspect language for advanced transactions
Parallel object monitors
Unanticipated partial behavioral reflection: Adapting applications at runtime
On dynamically-scoped crosscutting mechanisms
Programming Paradigms and Mind Metaphors: Convergence and Cross-fertilization in the Study of Cognition
A versatile kernel for distributed AOP
Aspects of composition in the reflex AOP kernel
Context-aware aspects
Declarative, formal, and extensible syntax definition for AspectJ - A case for scannerless generalized-LR parsing
Runtime bytecode transformation for Smalltalk
A versatile kernel for multi-language AOP
Sequential object monitors
Partial behavioral reflection: Spatial and temporal selection of reification
Altering Java semantics via bytecode manipulation

ConferencePaper (26)

A Mechanized Formalization of GraphQL
Trace-Relating Compiler Correctness and Secure Compilation
Existential types for relaxed noninterference
Polymorphic relaxed noninterference
A trustworthy mechanized formalization of R
Equivalences for Free Univalent Parametricity for Effective Transport
Abstracting Gradual Typing
An empirical study of goto in C code from github repositories
Gradual certified programming in Coq
Transactions on aspect-oriented software development XII
Aspectual session types
Compositional reasoning about aspect interference
Effect Capabilities for Haskell
Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice
On the use of type predicates in object-oriented software: The case of Smalltalk
Transactions on aspect-oriented software development XI
Cast Insertion Strategies for Gradually-Typed Objects
A practical monadic aspect weaver
A self-replication algorithm to flexibly match execution traces
An empirical study of the influence of static type systems on the usability of undocumented software
Taming aspects with membranes
Expressive Scoping of Distributed Aspects
Experimenting with language support for proximity in Ambient-Oriented Programming
Extending Omniscient Debugging to Support Aspect-Oriented Programming
Scalable omniscient debugging
Managing references upon object migration: Applying separation of concerns

Proyecto (12)

Gradual Reasoning About Programs: Typing, Analysis, and Verification
GECO=> Gradual Verification and Robust Proof Engineering for Coq
GRADUAL SOFTWARE VERIFICATION=> FOUNDATIONS AND APPLICATIONS
Reasoning About Effects in Aspect Languages
MODULAR AND ADAPTABLE SOFTWARE WITHOUT LOSING CONTROL
Reasoning about Aspect-oriented Programs and securIty in Distributed Systems
ENGINEERING AND COMPOSITION OF DOMAIN-SPECIFIC ASPECT LANGUAGES
Concurrency and Distribution in Aspect Languages
Latin American Network on Aspect-Oriented Software Development
Centro de Investigación de la Web
MODULARIZATION AND ADAPTATION OF COMPLEX AND DYNAMIC SOFTWARE SYSTEMS
Open Reflective Infrastructure for Open Networks
84
ERIC TANTER

Profesor Titular

Ciencias de la Computación

UNIVERSIDAD DE CHILE - DEPTO DE CIENCIAS DE LA COMPUTACION

Santiago, Chile

5
Paul Leger

Profesor Asociado

UNIVERSIDAD CATOLICA DEL NORTE -SEDE COQUIMBO

Coquimbo, Chile

4
JORGE SOTO

Full Professor

MATHEMATICS

UNIVERSIDAD DE CHILE

Santiago, Chile

3
Gina Luci

Docente

Educación

Universidad Autónoma de Chile

Santiago, Chile

3
Diego Cosmelli

Profesor Asociado y Sub-director de Investigación y Postgrado

Escuela de Psicología

PONTIFICIA UNIVERSIDAD CATOLICA DE CHILE

Santiago, Chile

2
Alexandre Bergel

Assistant Professor

DEPARTAMENTO DE LA CIENCIA DE LA COMPUTACIÓN (DCC)

Santiago, Chile

1
Matías Toro

Profesor Asistente

Departamento de Ciencias de la Computación

Universidad de Chile

Santiago, Chile