README⤓ .txt 2026-07-17T121634.146 000000000000808 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-07-15T060045.000 000000000023544 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-07-15T072202.000 000000000014672 Hewitt, Bishop, Steiger (1973). Concurrent computation via actors. Message passing only. No shared state. Foundation for distributed systems.
Ambient Calculus⤓ .md 2026-07-15T074030.000 000000000012904 Cardelli and Gordon (1998). Mobile computation in hierarchical spaces. Ambients as boundaries. Movement primitives. Foundation for mobile security.
Axiomatic Semantics⤓ .md 2026-07-15T065153.000 000000000016752 Floyd (1967), Hoare (1969). Program meaning via assertions. Preconditions and postconditions. Proof rules for constructs. Foundation for program verification.
Bigraphs⤓ .md 2026-07-15T071321.000 000000000015112 Milner (2001-2009). Unifying framework for mobile processes. Two structures: place graph (locality) and link graph (connectivity). Foundation for ubiquitous computing models.
Categorical Logic⤓ .md 2026-07-15T054120.000 000000000031128 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-07-15T072200.000 000000000014032 Berry and Boudol (1990). Computation as chemical reaction. Multiset of molecules. Reaction rules. Concurrent, non-deterministic. Foundation for process calculi semantics.
Coalgebraic Logic⤓ .md 2026-07-17T120407.600 000000000000872 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-07-17T120407.600 000000000000904 Giorgi Japaridze (2003). Games semantics for computation. Resources as game positions. Interactive computation. Beyond classical logic.
Constraint Logic Programming⤓ .md 2026-07-15T063115.000 000000000018888 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-07-15T065148.000 000000000014544 Scott and Strachey (1970s). Mathematical meaning of programs. Domains as semantic spaces. Compositionality: meaning from parts. Foundation for language semantics.
Domain Theory⤓ .md 2026-07-15T060302.000 000000000023312 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.
Equational Logic⤓ .md 2026-07-15T054026.000 000000000027832 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-07-15T071229.000 000000000015112 Lafont (1990). Graph rewriting for computation. Local interaction rules. Inherently parallel. Linear logic proof net execution.
Join Calculus⤓ .md 2026-07-16T005218.000 000000000034952 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-07-16T005313.000 000000000032056 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; Barendregt's Handbook treatment and Power–Thielecke's work on the categorical semantics. The point of the system is subtractive: what is the typed λ-calculus once function types are removed?
Logical Frameworks⤓ .md 2026-07-15T061544.000 000000000019112 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.
Matching Logic⤓ .md 2026-07-15T061752.000 000000000018712 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-07-15T074034.000 000000000014112 Păun (2000). Cell-inspired computation. Nested membranes. Object transformation. Foundation for natural computing.
Nominal Logic⤓ .md 2026-07-15T060703.000 000000000020080 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-07-15T065151.000 000000000015384 Plotkin (1981) SOS. Program meaning via execution rules. Small-step and big-step styles. Foundation for language implementation. Basis for type soundness proofs.
Petri Nets⤓ .md 2026-07-17T120407.600 000000000000832 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-07-15T073025.000 000000000012984 Milner, Parrow, Walker (1992). Mobile processes. Channel passing. Name binding. Foundation for mobile computation.
Pointer Logic⤓ .md 2026-07-17T120407.600 000000000000856 Reynolds (1970s), Sagiv-Reps-Wilhelm. Heap reasoning. Points-to analysis. Shape graphs. Foundation for heap verification.
Process Algebra⤓ .md 2026-07-17T120407.600 000000000000872 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.
Process Calculus⤓ .md 2026-07-17T120407.600 000000000000872 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-07-15T052839.000 000000000030352 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-07-16T005218.000 000000000033360 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-07-15T062342.000 000000000018360 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-07-16T005313.000 000000000031200 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-17T120407.600 000000000000824 Not sufficient: A logic for proving program correctness (Verification). A type system as such (Type). A logic for natural-language meaning (Semantics).