Publications by Nada Amin | EPFL Graph Search

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. In particular, objects can contain type members, which can be selected as ...

High level data structures are a cornerstone of modern programming and at the same time stand in the way of compiler optimizations. In order to reason about user or library-defined data structures, compilers need to be extensible. Common mechanisms to exte ...

Scala-Virtualized extends the Scala language to better support hosting embedded DSLs. Scala is an expressive language that provides a flexible syntax, type-level computation using implicits, and other features that facilitate the development of em- bedded ...

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. An essential ingredient of this unification is the concept of objects wit ...

We propose a new type-theoretic foundation of Scala and languages like it: the Dependent Object Types (DOT) calculus. DOT models Scala’s path-dependent types, abstract type members and its mixture of nominal and structural typing through the use of reﬁneme ...

Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasonin ...

This article presents a modular, flow-insensitive type-and- effect system for purity with lightweight annotations. It does not enforce a global programming discipline and allows ar- bitrary effects to occur in impure parts of the program. The system is des ...

Scala's type system unifies aspects of ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, ty ...

Probabilistic programming is a powerful high-level paradigm for probabilistic modeling and inference. We present Odds, a small domain-specific language (DSL) for probabilistic programming, embedded in Scala. Odds provides first-class support for random var ...

Developing rich web applications requires mastering different environments on the client and server sides. While there is considerable choice on the server-side, the client-side is tied to JavaScript, which poses substantial software engineering challenges ...

We present short programs that demonstrate the unsoundness of Java and Scala’s current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down)casting. Fortunately, paramet ...

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculu ...

We present the design and implementation of a SQL query processor that outperforms existing database systems and is written in just about 500 lines of Scala code - a convincing case study that high-level functional programming can handily beat C for system ...

We present short programs that demonstrate the unsoundness of Java and Scala's current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down) casting. Fortunately, parame ...

Scala’s type system unifies aspects of ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, ty ...

Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus D-

Nada Amin

Chat with Graph Search

LMS-Verify: Abstraction without Regret for Verified Systems Programming’

Dependent Object Types

Optimizing Data Structures in High-Level Programs New Directions for Extensible Compilers based on Staging

Scala-Virtualized: Linguistic Reuse for Deep Embeddings

Foundations of Path-Dependent Types

Dependent Object Types

Stoic: Towards Disciplined Capabilities

A Flow-Insensitive, Modular Effect System for Purity

Type Soundness for Dependent Object Types (DOT)

What are the Odds? Probabilistic programming in Scala

JavaScript as an Embedded DSL

Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers

Type Soundness Proofs with Definitional Interpreters

Functional Pearl: A SQL to C Compiler in 500 Lines of Code

Java and Scala's Type Systems are Unsound The Existential Crisis of Null Pointers

Type Soundness for Dependent Object Types

The Essence of Dependent Object Types