Matthias Felleisen is a German-American computer science professor and author. He grew up in Germany and immigrated to the US in his twenties. He received his PhD from Indiana University under the direction of Daniel P. Friedman.
In computer science, a type class is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T.
The International Conference on Functional Programming (ICFP) is an annual academic conference in the field of computer science sponsored by the ACM SIGPLAN, in association with IFIP Working Group 2.8. The conference focuses on functional programming and related areas of programming languages, logic, compilers and software development.
In computer science, pointer analysis, or points-to analysis, is a static code analysis technique that establishes which pointers, or heap references, can point to which variables, or storage locations. It is often a component of more complex analyses such as escape analysis. A closely related technique is shape analysis.
The Geometry of Interaction (GoI) was introduced by Jean-Yves Girard shortly after his work on linear logic. In linear logic, proofs can be seen as various kinds of networks as opposed to the flat tree structures of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard devised a criterion involving trips in the network. Trips can in fact be seen as some kind of operator acting on the proof. Drawing from this observation, Girard described directly this operator from the proof and has given a formula, the so-called execution formula, encoding the process of cut elimination at the level of operators.
Boomerang is a programming language for writing lenses—well-behaved bidirectional transformations —that operate on ad-hoc, textual data formats.
Hermes is a language for distributed programming that was developed at IBM's Thomas J. Watson Research Center from 1986 through 1992, with an open-source compiler and run-time system. Hermes' primary features included:
In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as . Refinement types are thus related to behavioral subtyping.
In computer science, region-based memory management is a type of memory management in which each allocated object is assigned to a region. A region, also called a zone, arena, area, or memory context, is a collection of allocated objects that can be efficiently reallocated or deallocated all at once. Like stack allocation, regions facilitate allocation and deallocation of memory with low overhead; but they are more flexible, allowing objects to live longer than the stack frame in which they were allocated. In typical implementations, all objects in a region are allocated in a single contiguous range of memory addresses, similarly to how stack frames are typically allocated.
In program analysis, a polyvariant or context-sensitive analysis analyzes each function multiple times—typically once at each call site—to improve the precision of the analysis. Polyvariance is common in data-flow and pointer analyses.
F* is a functional programming language inspired by ML and aimed at program verification. Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript.
Gradual typing is a type system in which some variables and expressions may be given types and the correctness of the typing is checked at compile time and some expressions may be left untyped and eventual type errors are reported at runtime. Gradual typing allows software developers to choose either type paradigm as appropriate, from within a single language. In many cases gradual typing is added to an existing dynamic language, creating a derived language allowing but not requiring static typing to be used. In some cases a language uses gradual typing from the start.
In computer science, Steensgaard's algorithm is a scalable, flow-insensitive, algorithm for pointer analysis. It is often used in compilers, due to its speed. In its original formulation, this algorithm was field-, context-, and array-insensitive.
David Bacon is an American computer programmer.
Value numbering is a technique of determining when two computations in a program are equivalent and eliminating one of them with a semantics-preserving optimization.
Lucy Gilbert is an American computer programmer and video game developer. She worked for Atari, Inc. via General Computer Corporation and developed computer graphics software for Autographix.
In computer science, choreographic programming is a programming paradigm where programs are compositions of interactions among multiple concurrent participants.
Ilya Sergey is a Russian computer scientist and an Associate Professor at the School of Computing at the National University of Singapore, where he leads the Verified Systems Engineering lab. Sergey does research in programming language design and implementation, software verification, distributed systems, program synthesis, and program repair. He is known for designing the Scilla programming language for smart contracts. He is the author of the free online book, Programs and Proofs: Mechanizing Mathematics with Dependent Types, Lecture notes with exercises, which provides an introduction to the basic concepts of mechanized reasoning and interactive theorem proving using Coq.
