Related Research Articles
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program.
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.
The National Institute for Research in Digital Science and Technology (Inria) is a French national research institution focusing on computer science and applied mathematics. It was created under the name French Institute for Research in Computer Science and Automation (IRIA) in 1967 at Rocquencourt near Paris, part of Plan Calcul. Its first site was the historical premises of SHAPE, which is still used as Inria's main headquarters. In 1980, IRIA became INRIA. Since 2011, it has been styled Inria.
In theoretical computer science, the π-calculus is a process calculus. The π-calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe concurrent computations whose network configuration may change during the computation.
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.
In computer science, the process calculi are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes. They also provide algebraic laws that allow process descriptions to be manipulated and analyzed, and permit formal reasoning about equivalences between processes. Leading examples of process calculi include CSP, CCS, ACP, and LOTOS. More recent additions to the family include the π-calculus, the ambient calculus, PEPA, the fusion calculus and the join-calculus.
In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability of a program, algorithm, or problem into order-independent or partially-ordered components or units of computation.
The actor model in computer science is a mathematical model of concurrent computation that treats an actor as the basic building block of concurrent computation. In response to a message it receives, an actor can: make local decisions, create more actors, send more messages, and determine how to respond to the next message received. Actors may modify their own private state, but can only affect each other indirectly through messaging.
In computer science, the Actor model and process calculi are two closely related approaches to the modelling of concurrent digital computation. See Actor model and process calculi history.
Join Java is a programming language based on the join-pattern that extends the standard Java programming language with the join semantics of the join-calculus. It was written at the University of South Australia within the Reconfigurable Computing Lab by Dr. Von Itzstein.
Concurrent computing is a form of computing in which several computations are executed concurrently—during overlapping time periods—instead of sequentially—with one completing before the next starts.
The actor model and process calculi share an interesting history and co-evolution.
JoCaml is an experimental functional programming language derived from OCaml. It integrates the primitives of the join-calculus to enable flexible, type-checked concurrent and distributed programming. The current version of JoCaml is a re-implementation of the now unmaintained JoCaml made by Fabrice Le Fessant, featuring a modified syntax and improved OCaml compatibility compared to the original.
ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet.
Join-patterns provides a way to write concurrent, parallel and distributed computer programs by message passing. Compared to the use of threads and locks, this is a high level programming model using communication constructs model to abstract the complexity of concurrent environment and to allow scalability. Its focus is on the execution of a chord between messages atomically consumed from a group of channels.
Elixir is a functional, concurrent, high-level general-purpose programming language that runs on the BEAM virtual machine, which is also used to implement the Erlang programming language. Elixir builds on top of Erlang and shares the same abstractions for building distributed, fault-tolerant applications. Elixir also provides tooling and an extensible design. The latter is supported by compile-time metaprogramming with macros and polymorphism via protocols.
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.
In type theory, session types are used to ensure correctness in concurrent programs. They guarantee that messages sent and received between concurrent programs are in the expected order and of the expected type. Session type systems have been adapted for both channel and actor systems.
References
- ↑ Cedric Fournet, Georges Gonthier (1995). "The reflexive CHAM and the join-calculus".
{{cite journal}}: Cite journal requires|journal=(help), pg. 1 - ↑ Cedric Fournet, Georges Gonthier (1995). "The reflexive CHAM and the join-calculus".
{{cite journal}}: Cite journal requires|journal=(help), pg. 2 - ↑ Cedric Fournet, Georges Gonthier (1995). "The reflexive CHAM and the join-calculus".
{{cite journal}}: Cite journal requires|journal=(help), pg. 19 - ↑ Petricek, Tomas. "TryJoinads (IV.) - Concurrency using join calculus". tomasp.net. Retrieved 2023-01-24.
- ↑ Cedric Fournet, Georges Gonthier (2000). "The Join Calculus: A Language for Distributed Mobile Programming": 268–332.
{{cite journal}}: Cite journal requires|journal=(help) - ↑ "JErlang: Erlang with Joins". Archived from the original on 2017-12-08. Retrieved 2015-04-18.
- ↑ Join Python, Join-calculus for Python by Mattias Andree
- ↑ Yigong Liu - Join-Asynchronous Message Coordination and Concurrency Library
