README⤓ .txt 2026-08-19T232042.000 000000000007112 Logics and calculi that give formal meaning to the behavior of programs and processes: how computation proceeds, what a program denotes, and how concurrent and mobile systems interact. The unifying concern is the semantics of computation rather than the proof of its correctness.
Abstract Interpretation⤓ .md 2026-10-22T165042.936 000000000000944 Cousot and Cousot introduced abstract interpretation (1977). Framework for sound approximation of program semantics. Abstract domains capture properties of interest. Galois connections formalize soundness. Foundation for static analysis tools (Astrée, Polyspace, Infer).
Actor Model⤓ .md 2026-08-20T075107.000 000000000043112 Carl Hewitt, Peter Bishop and Richard Steiger, "A Universal Modular ACTOR Formalism for Artificial Intelligence" (IJCAI 1973), growing out of Planner and the message-passing discipline of Smalltalk. Baker and Hewitt (1977) stated the laws for communicating parallel processes. Greif (1975) gave the first operational semantics, Clinger (1981) the first denotational one, and Agha (1986) the configuration-based operational theory that later work builds on; Agha, Mason, Smith and Talcott (1997) supplied a full equational theory.
Ambient Calculus⤓ .md 2026-10-22T085445.000 000000000028512 Cardelli and Gordon (1998). Mobile computation in hierarchical spaces. Ambients as boundaries. Movement primitives. Foundation for mobile security.
Axiomatic Semantics⤓ .md 2026-08-20T075720.000 000000000030616 Floyd (1967), Hoare (1969). Program meaning via assertions. Preconditions and postconditions. Proof rules for constructs. Foundation for program verification.
Bigraphs⤓ .md 2026-08-20T080046.000 000000000030072 Milner (2001-2009). Unifying framework for mobile processes. Two structures: place graph (locality) and link graph (connectivity). Foundation for ubiquitous computing models.
Call-by-Push-Value⤓ .md 2026-10-22T180154.561 000000000000896 Paul Blain Levy, "Call-by-push-value: a subsuming paradigm" (TLCA 1999, Springer LNCS 1581, pp. 228–242), developed through his thesis (Queen Mary, University of London, 2001) into the book Call-By-Push-Value: A Functional/Imperative Synthesis (Springer, Semantic Structures in Computation, 2003); the journal statement of the subsumption is "Call-by-push-value: decomposing call-by-value and call-by-name" (Higher-Order and Symbolic Computation 19(4), 2006, pp. 377–414). The adjoint decomposition has a precedent in Nick Benton's mixed linear/non-linear logic LNL (CSL 1994), which split linear logic's ! into an adjunction; Levy's calculus does the same to the monad of Moggi's "Notions of computation and monads" (Information and Computation, 1991).
Categorical Logic⤓ .md 2026-10-22T180154.561 000000000000872 F. William Lawvere pioneered categorical logic (1960s), showing logical systems correspond to categorical structures. The topos concept (Grothendieck for algebraic geometry, Lawvere-Tierney for logic) provides a universe for mathematics beyond sets. Unifies logic, type theory, and geometry. Foundational for Homotopy Type Theory.
Chemical Abstract Machine⤓ .md 2026-10-22T165042.936 000000000000952 Gérard Berry and Gérard Boudol, "The chemical abstract machine" (POPL 1990; journal version in Theoretical Computer Science 96, 1992), building on the Gamma multiset-rewriting formalism of Banâtre and Le Métayer. The aim was a presentation of operational semantics for concurrency in which no syntactic ordering has to be undone before a step can be taken. Milner's reaction-based presentation of the π-calculus adopted the chemical style, and Fournet and Gonthier's reflexive CHAM (1996) is the join calculus.
Coalgebraic Logic⤓ .md 2026-08-20T013045.000 000000000050984 Coalgebra as a general theory of state-based systems: Aczel (non-well-founded sets, 1988), Rutten (universal coalgebra, 2000). Coalgebraic modal logic: Moss (1999), Pattinson, Kupke, Cîrstea. The uniform framework in which transition systems, automata, streams, and probabilistic systems are all coalgebras, and modal logics are their specification languages.
Computability Logic⤓ .md 2026-10-22T085636.000 000000000038616 Giorgi Japaridze (2003). Games semantics for computation. Resources as game positions. Interactive computation. Beyond classical logic.
Concurrent Constraint Programming⤓ .md 2026-10-22T180154.561 000000000001016 Vijay Saraswat's Carnegie Mellon dissertation (1989), published as Concurrent Constraint Programming (MIT Press, 1993). Saraswat and Rinard, "Concurrent constraint programming" (POPL 1990). Saraswat, Rinard, and Panangaden, "The semantic foundations of concurrent constraint programming" (POPL 1991). Subsumes and generalizes concurrent logic programming and constraint logic programming.
Constraint Logic Programming⤓ .md 2026-08-20T082242.000 000000000031752 Jaffar and Lassez introduced CLP scheme (1987). Extends logic programming with constraint solving. Combines Prolog-style reasoning with domain-specific solvers. Foundation for constraint satisfaction and optimization. Systems: CLP(R), CLP(FD), ECLiPSe, SICStus.
Denotational Semantics⤓ .md 2026-10-22T165042.936 000000000000928 Scott and Strachey (1970s). Mathematical meaning of programs. Domains as semantic spaces. Compositionality: meaning from parts. Foundation for language semantics.
Domain Theory⤓ .md 2026-10-22T090413.000 000000000046272 Dana Scott introduced domains (1969-70) to give semantics to the lambda calculus. Solves: D ≅ D → D (types isomorphic to their function space). Continuous lattices and dcpos provide mathematical foundation. Scott and Strachey developed denotational semantics. Foundational for programming language semantics.
Edinburgh Logical Framework⤓ .md 2026-10-22T085113.000 000000000030504 Harper, Honsell, Plotkin introduced LF (Edinburgh Logical Framework, 1993). Meta-languages for defining logics. Represent syntax, judgments, and derivations. Encode object logics faithfully. Foundation for Twelf, Beluga, and other systems.
Equational Logic⤓ .md 2026-08-20T082725.000 000000000037392 Birkhoff's completeness theorem for equational logic (1935). Term rewriting developed by Knuth and Bendix (1970), providing algorithms for equational reasoning. Foundation for algebraic specification (OBJ, Maude, CafeOBJ) and functional programming. Connects algebra, logic, and computation.
Interaction Nets⤓ .md 2026-10-22T090714.000 000000000028176 Lafont (1990). Graph rewriting for computation. Local interaction rules. Inherently parallel. Linear logic proof net execution.
Join Calculus⤓ .md 2026-10-22T165042.936 000000000000856 Cédric Fournet and Georges Gonthier, "The reflexive CHAM and the join-calculus" (POPL 1996), and Fournet's thesis (1998). Built from the chemical abstract machine to answer a question the π-calculus leaves open: what does a process calculus look like if every construct is directly implementable in a distributed setting with no shared memory and no atomic broadcast?
Kappa Calculus⤓ .md 2026-10-22T085732.000 000000000043440 Masahito Hasegawa, "Decomposing typed lambda calculus into a couple of categorical programming languages" (CTCS 1995), which introduced κ as the first-order half of a decomposition; Power and Thielecke's κ-categories supply the categorical semantics. The point of the system is subtractive: what is the typed λ-calculus once function types are removed?
Logical Frameworks⤓ .md 2026-10-22T085113.000 000000000030504 Harper, Honsell, Plotkin introduced LF (Edinburgh Logical Framework, 1993). Meta-languages for defining logics. Represent syntax, judgments, and derivations. Encode object logics faithfully. Foundation for Twelf, Beluga, and other systems.
Markov Algorithms⤓ .md 2026-10-22T180154.561 000000000000888 Andrei Andreevich Markov — the younger, son of the probabilist — announced normal algorithms in "Teoriya algorifmov" (Trudy Matematicheskogo Instituta imeni V. A. Steklova 38, 1951, pp. 176–189; English translation "The theory of algorithms", American Mathematical Society Translations, series 2, volume 15, 1960, pp. 1–14) and developed them in the monograph Teoriya algorifmov (Trudy Mat. Inst. Steklova 42, 1954; English translation Theory of Algorithms, Israel Program for Scientific Translations, Jerusalem 1961, reissued 1962; second edition with Nikolai M. Nagorny, Nauka 1984, English edition Kluwer 1988). The unsolvability results came first: two 1947 Doklady Akademii Nauk notes, "Nevozmozhnost' nekotorykh algorifmov v teorii assotsiativnykh sistem" (On the impossibility of certain algorithms in the theory of associative systems), settled the word problem for finitely presented semigroups — Thue's problem — in the same year as Post and independently of him, and the 1951 note "Nevozmozhnost' algorifmov raspoznavaniya nekotorykh svoistv assotsiativnykh sistem" extended the impossibility to the algorithmic recognition of properties of associative systems.
Matching Logic⤓ .md 2026-08-20T084937.000 000000000039640 Roșu introduced Matching Logic (2017). Unifying framework: FOL, modal logics, separation logic, rewriting. Patterns match (sets of) elements. Foundation for K Framework. Aims to be "the" logic for programming language semantics.
Membrane Computing⤓ .md 2026-10-22T165042.936 000000000000896 Gheorghe Păun, "Computing with membranes", Turku Centre for Computer Science report 208 (1998), published in the Journal of Computer and System Sciences 61 (2000). The model abstracts the compartmental architecture of the living cell: chemical species become objects, compartments become membranes, reactions become multiset rewriting rules. It established membrane computing as a branch of natural computing beside DNA computing and evolutionary computation, and the variants are catalogued in the Handbook of Membrane Computing (Păun, Rozenberg, Salomaa, 2010).
Nominal Logic⤓ .md 2026-10-22T085140.000 000000000030664 Gabbay and Pitts introduced nominal techniques (1999-2002). Logic for name-binding and α-equivalence. Names (atoms) can be swapped and fresh names generated. Addresses variable binding in syntax. Foundation for Nominal Isabelle and other tools.
Operational Semantics⤓ .md 2026-08-20T095425.000 000000000042008 Gordon Plotkin, "A Structural Approach to Operational Semantics", Aarhus technical report DAIMI FN-19 (1981), reprinted in the Journal of Logic and Algebraic Programming (2004). The point of structural operational semantics is that the transition relation is defined by inference rules following the syntax, so a program's behaviour is derived from its parts. Gilles Kahn's natural semantics (1987) is the big-step counterpart. Felleisen and Hieb (1992) recast reduction with evaluation contexts, and Wright and Felleisen (1994) turned the whole apparatus into the standard syntactic proof of type soundness.
PCF⤓ .md 2026-10-22T180154.561 000000000000672 Dana Scott, "A type-theoretical alternative to ISWIM, CUCH, OWHY", written at Oxford in 1969, circulated as a manuscript for twenty-four years, and published in Theoretical Computer Science 121 (1993): a typed logic of computable functions with fixed points, proposed against the untyped calculi its title mocks. Gordon Plotkin, "LCF considered as a programming language" (Theoretical Computer Science 5, 1977, pp. 223–255), took the term language of Scott's logic, named it PCF, gave it an operational semantics, and proved the adequacy and full-abstraction theorems that set the field's agenda; Robin Milner, "Fully abstract models of typed λ-calculi" (Theoretical Computer Science 4, 1977, pp. 1–22), constructed the fully abstract model and left open the problem of describing it without syntax.
Petri Nets⤓ .md 2026-08-20T090923.000 000000000038976 Carl Adam Petri, doctoral thesis "Kommunikation mit Automaten" (1962). The foundational model of concurrency with true (non-interleaving) parallelism. Basis for workflow, protocol, and manufacturing-system analysis; extended into colored, timed, and stochastic variants.
Pi Calculus⤓ .md 2026-08-20T091633.000 000000000028736 Milner, Parrow, Walker (1992). Mobile processes. Channel passing. Name binding. Foundation for mobile computation.
Pointer Logic⤓ .md 2026-10-22T165042.936 000000000000856 Burstall's 1972 treatment of "distinct nonrepeating tree systems" is the first attempt to reason about programs that alter linked structures. Jones and Muchnick (1979, 1981) introduced the flow-analytic version, abstracting the heap by k-limiting; Chase, Wegman and Zadeck (1990) added storage shape graphs. Sagiv, Reps and Wilhelm gave the theory its general form in "Solving shape-analysis problems in languages with destructive updating" (1998) and "Parametric shape analysis via 3-valued logic" (2002), implemented as TVLA. Reynolds's separation logic (2002), developed with O'Hearn and Yang, is the deductive counterpart.
Post Canonical Systems⤓ .md 2026-10-22T165042.936 000000000000928 Emil Post, "Formal reductions of the general combinatorial decision problem" (American Journal of Mathematics 65, 1943, pp. 197–215), defining canonical and normal systems and proving the normal-form theorem. The formalism is two decades older than its publication: Post reached it, together with the unsolvability it implies, in his Princeton work of the early 1920s, published only as "Absolutely unsolvable problems and relatively undecidable propositions — account of an anticipation" in Martin Davis's The Undecidable (Raven Press, 1965). "Recursive unsolvability of a problem of Thue" (Journal of Symbolic Logic 12, 1947, pp. 1–11) carried the formalism into algebra, settling the word problem for semigroups; Markov proved the same result independently. The second life began when Allen Newell and Herbert Simon made production rules the medium of their cognitive theory in Human Problem Solving (1972); Charles Forgy's Carnegie Mellon thesis "On the efficient implementation of production systems" (1979) and the Carnegie Mellon OPS languages culminating in his OPS5 made production systems a programming practice, and "Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem" (Artificial Intelligence 19, 1982, pp. 17–37) supplied its match algorithm.
Process Algebra⤓ .md 2026-10-22T090936.000 000000000041552 Robin Milner developed CCS (Calculus of Communicating Systems, 1980) and later the π-calculus (1992). Tony Hoare developed CSP (Communicating Sequential Processes, 1978, 1985). Jan Bergstra and Jan Willem Klop developed ACP (Algebra of Communicating Processes, 1984). These provide algebraic frameworks for concurrent and distributed systems.
Relational Algebra⤓ .md 2026-08-20T102314.000 000000000037048 Edgar F. Codd introduced the relational model and relational algebra (1970) at IBM. Provided a mathematical foundation for database systems, replacing navigational models (hierarchical, network) with declarative queries. Basis for SQL. Turing Award 1981.
Relational Calculus⤓ .md 2026-10-22T090146.000 000000000038312 E. F. Codd, "A relational model of data for large shared data banks" (1970) and "Relational completeness of data base sublanguages" (1972), where the calculus and the theorem relating it to the algebra both appear. Lacroix and Pirotte (1977) gave the domain variant. The founding result of database theory, and the reason SQL looks like logic and runs like algebra.
Rewriting Logic⤓ .md 2026-10-22T090714.000 000000000030160 Meseguer introduced rewriting logic (1992). Unifies many computational paradigms. States as algebraic terms, transitions as rewrite rules. Foundation for Maude language. Reflects concurrent systems, OO programming, real-time systems.
Rho Calculus⤓ .md 2026-10-22T165042.936 000000000000848 Horatiu Cirstea and Claude Kirchner, "The rewriting calculus, parts I and II" (Logic Journal of the IGPL, 2001), with the ELAN system as the practical setting; developed with Liquori, Wack, and Bertolissi through the 2000s. The aim: λ-calculus and term rewriting are the two computational models of the field and are always presented separately, so give them one calculus.
CRITERIA⤓ .txt 2026-07-15T162258.000 000000000007712 Not sufficient: A logic for proving program correctness (Verification). A type system as such (Type). A logic for natural-language meaning (Semantics).