Related Research Articles
ML is a functional programming language. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the data types of most expressions without requiring explicit type annotations, and ensures type safety; there is a formal proof that a well-typed ML program does not cause runtime type errors. ML provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying. While a general-purpose programming language, ML is used heavily in programming language research and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing, automated theorem proving, and formal verification.
OCaml is a general-purpose, high-level, multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez, and others.
Arthur John Robin Gorell Milner was a British computer scientist, and a Turing Award winner.
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular for writing compilers, for programming language research, and for developing theorem provers.
Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics.
The UCPH Department of Computer Science is a department in the Faculty of Science at the University of Copenhagen (UCPH). It is the longest established department of Computer Science in Denmark and was founded in 1970 by Turing Award winner Peter Naur. As of 2021, it employs 82 academic staff, 126 research staff and 38 support staff. It is consistently ranked the top Computer Science department in the Nordic countries, and in 2017 was placed 9th worldwide by the Academic Ranking of World Universities.
In computer science, type safety and type soundness are the extent to which a programming language discourages or prevents type errors. Type safety is sometimes alternatively considered to be a property of facilities of a computer language; that is, some facilities are type-safe and their usage will not result in type errors, while other facilities in the same language may be type-unsafe and a program using them may encounter type errors. The behaviors classified as type errors by a given programming language are usually those that result from attempts to perform operations on values that are not of the appropriate data type, e.g., adding a string to an integer when there's no definition on how to handle this case. This classification is partly based on opinion.
SIGPLAN is the Association for Computing Machinery's Special Interest Group on programming languages.
John Charles Reynolds was an American computer scientist.
Robert William "Bob" Harper, Jr. is a computer science professor at Carnegie Mellon University who works in programming language research. Prior to his position at Carnegie Mellon, Harper was a research fellow at the University of Edinburgh.
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.
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, polymorphic recursion refers to a recursive parametrically polymorphic function where the type parameter changes with each recursive invocation made, instead of staying constant. Type inference for polymorphic recursion is equivalent to semi-unification and therefore undecidable and requires the use of a semi-algorithm or programmer-supplied type annotations.
George Ciprian Necula is a Romanian computer scientist, engineer at Google, and former professor at the University of California, Berkeley who does research in the area of programming languages and software engineering, with a particular focus on software verification and formal methods. He is best known for his Ph.D. thesis work first describing proof-carrying code, a work that received the 2007 SIGPLAN Most Influential POPL Paper Award.
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.
Haskell is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell has pioneered a number of programming language features such as type classes, which enable type-safe operator overloading, and monadic input/output (IO). It is named after logician Haskell Curry. Haskell's main implementation is the Glasgow Haskell Compiler (GHC).
SIGNAL is a programming language based on synchronized data-flow : a process is a set of equations on elementary flows describing both data and control.
In programming languages with Hindley-Milner type inference and imperative features, in particular the ML programming language family, the value restriction means that declarations are only polymorphically generalized if they are syntactic values. The value restriction prevents reference cells from holding values of different types and preserves type safety.
Futhark is a functional data parallel array programming language originally developed at UCPH Department of Computer Science (DIKU) as part of the HIPERFIT project. It focuses on enabling data parallel programs written in a functional style to be executed with high performance on massively parallel hardware, in particular on graphics processing units (GPUs). Futhark is strongly inspired by NESL, and its implementation uses a variant of the flattening transformation, but imposes constraints on how parallelism can be expressed in order to enable more aggressive compiler optimisations. In particular, irregular nested data parallelism is not supported.
References
- ↑ M. Tofte: Compiler Generators: What They Can Do, What They Might Do, and What They Will Probably Never Do. Springer-Verlag 1990
- ↑ R. Milner, M. Tofte, R. Harper: The Definition of Standard ML, MIT Press 1990, second edition 1997
- ↑ M. Tofte and J.-P. Talpin: Implementation of the Typed Call-by-Value lambda-calculus using a Stack of Regions, In Proceedings of POPL 1994
- ↑ P.H. Eidorff, F. Henglein, C. Mossin, H. Niss, M.H. Sørensen, M. Tofte: AnnoDomini: From type theory to year 2000 conversion tool. In Proceedings of POPL 1999
- ↑ Tofte, Mads. "Jeg forlader nu Danmark i protest mod de ekstreme regler, der forhindrer, at min afrikanske adoptivdatter kommer til landet". Politiken. Retrieved 28 January 2019.
