|
abstract
|
Describing things on a level without regard to detail, such as implementation or efficiency.
|
5
|
|
abstract data type
|
A type defined not by its internal representation but by the operations
that can be performed on it. Type-theoretically encoded as an existential type.
|
9
|
|
abstract machine
|
A state machine used to specify evaluation of a program where we care about cost.
|
5
|
|
abstract syntax
|
A representation of a language's syntax with no ambiguity, and with superfluous information removed. Usually represented as a tree data structure rather than a list of characters or tokens.
|
1
2
|
|
abstraction
|
A form of term that introduces a new bound variable in higher-order abstract syntax, see λ-abstraction. Also can refer to the general notion of removing detail from a specification of a program.
|
2
|
|
abstraction function
|
A function mapping concrete states to abstract states, forms the basis of a simulation relation to prove refinement.
|
5
|
|
ad-hoc polymorphism
|
Referring to multiple different values by the same name, with the exact implementation chosen during type checking. Common implementations are based on type classes.
|
9
|
|
admissible
|
An inference rule is admissible to a language $L$ if adding the rule to the language definition does not change $L$.
|
2
|
|
ADT
|
An abstract data type. Never refers to an algebraic data type.
|
9
|
|
algebraic data type
|
A type comprised of sum types and product types.
|
7
|
|
ambiguity
|
A language $L$ is ambiguous if there exists a string $s$ that can be proven to be part of $L$ in two or more ways.
|
2
|
|
antisymmetric
|
A property of a relation $R$ where $a\ R\ b$ and $b\ R\ a$ implies $a = b$.
|
|
|
application
|
A function being "called", i.e. given arguments to produce its result. An application is written $e_1\ e_2$, where the expression $e_1$ denotes a function and $e_2$ denotes the argument being passed to that function.
|
3
|
|
arity
|
Number of objects on which a function, relation or judgement operates.
|
3
|
|
assembly language
|
A type of imperative language where each command corresponds to exactly one machine instruction.
|
4
|
|
assertion
|
A logical proposition that may involve variables from a program's mutable state.
|
4
|
|
assignment
|
A statement $x := e$ that updates the mutable variable $x$ to have the value resulting from $e$.
|
4
|
|
associativity
|
A property of an operator (here written $\cdot$) where $A \cdot B \cdot C = A \cdot (B \cdot C) = (A \cdot B) \cdot C$. Allows us to rearrange parentheses at will. Examples: addition, multiplication.
|
2
|
|
atomic
|
A sequence of steps are atomic if they cannot be interrupted, and can be viewed as effectively one step by any external observer. For example, a critical section.
|
10
|
|
axiom
|
An inference rule with no premises. Always holds.
|
2
|
|
axiomatic semantics
|
The specification of a language's dynamic semantics via the construction of a proof calculus to
allow correctness of a program to be verified.
|
3
|
|
Backus-Naur Form
|
A compact recursive notation used to describe a language's grammar. For example, $M ::= \epsilon\ \vert\ \texttt{(} M \texttt{)}\ \vert\ M M$ is the language of matching parentheses.
|
1
|
|
base case
|
An elementary proof case that is derived from an axiom in an inductive proof.
|
2
|
|
behaviour
|
An infinite sequence of states, a generalised notion of a trace.
|
7
|
|
big-O notation
|
Describing the asymptotic behaviour of functions on real numbers with an upper bound.
|
5
|
|
big-step semantics
|
The specification of evaluation in dynamic semantics according to a relation $\Downarrow \subseteq E \times V$ where $E$ is the set of evaluable expressions and $V$ is the set of values.
|
3
|
|
bijection
|
An injective and surjective mapping between two sets.
|
|
|
binary operator
|
A function on a set $A$ that takes two elements of $A$ and produces an element of $A$. Examples: addition, multiplication, subtraction, division, implication, conjunction, disjunction.
|
|
|
binder
|
An expression that contains the binding occurrence of a variable, for example let expressions.
|
2
|
|
binding occurrence
|
The use of a variable name that defines it, or gives it its value. For example, in λ-abstractions or let expressions.
|
2
|
|
boolean
|
The set containing $\{ \top, \bot \}$.
|
|
|
bound
|
A variable is bound in an expression $e$ if it is defined or introduced in the expression $e$, i.e. its binding occurrence is in $e$.
|
2
|
|
boxing
|
A means of implementing parametric polymorphism where all objects are stored on the stack uniformly as a pointer to a heap object.
|
8
|
|
C-machine
|
A refinement of the M-machine where control flow is made explicit with a stack of one-hole contexts. All rules are axioms.
|
5
|
|
call-by-name
|
The evaluation strategy where β-reduction is evaluated before function arguments. Can be computationally expensive.
|
3
|
|
call-by-need
|
An evaluation strategy that depends on graph reduction that effectively optimises call-by-name execution to be computationally inexpensive.
|
3
|
|
call-by-value
|
An evaluation strategy where function arguments are evaluated before β-reduction. Also called strict evaluation.
|
3
|
|
capture
|
The problem that arises in a substitution $e[x:=t]$ whenever a variable that appears in $t$ is also bound in $e$. For example let x = 5 in y + 1 applying the substitution $[y := x]$.
|
2
|
|
cartesian product
|
The set $A \times B$ contains sets of pairs $\{ (a, b)\ |\ a \in A \land b \in B \}$.
|
|
|
checked exceptions
|
A form of exceptions where the possibility of a raise is tracked in the type system.
|
7
|
|
class instance
|
A set of implementations of methods for a particular type class and type.
|
9
|
|
closure
|
A representation of a function value which includes the function body and an environment containing all the
values in scope at the time the function was defined.
|
5
|
|
code generator
|
The final phase of a compiler, which produces appropriate code in a lower-level language such as machine code.
|
1
|
|
codomain
|
The output set of a function.
|
|
|
coercion
|
An injective mapping from a subtype to a supertype.
|
9
|
|
commit phase
|
The phase of transaction execution in transactional memory where all changes to transactional variables are saved to the shared variables.
|
10
|
|
commutative semiring
|
An algebraic structure consisting of a set $U$ and two operators $+$ and $\times$, with two identity elements $0 \in U$ and $1 \in U$ that behave analogously to the natural numbers in terms of associativity, commutativity, left and right-identity.
|
7
|
|
commutativity
|
A property of an operator (here written $\cdot$) where $A \cdot B = B \cdot A$. Allows us to move terms around at will. Examples: addition, multiplication.
|
|
|
compiler
|
A program which, given program source code, translates the program into a lower-level language, usually machine code. Consists of a lexer, parser, semantic analyser, code generator and sometimes an optimiser.
|
1
|
|
complete execution
|
An execution that is maximal and ends in a final state.
|
3
|
|
completed trace
|
See complete execution.
|
3
|
|
compositional
|
A general mathematical adjective that says that a mathematical object can be constructed by the combination of other objects, regardless of those objects' particular characteristics.
|
3
|
|
conclusion
|
The judgement that is proven by a particular inference rule.
|
2
|
|
concrete
|
More precise, including detail. Opposite of abstract.
|
5
|
|
concrete syntax
|
A representation of a language's syntax that corresponds closely to what the programmer would write in their editor, as opposed to abstract syntax which is an unambiguous tree representation.
|
2
|
|
concurrency
|
An abstraction for the programmer, allowing programs to be structured as
multiple threads of control, called processes. They may communicate
in various ways.
|
9
10
|
|
confluence
|
Property of a reduction that states that a term $A$ can be reduced in one way to $B$ and in another way to $C$, then $B$ and $C$ must both be reducible to a common term $D$.
|
3
|
|
congruence
|
Property of a reduction that states that the reduction can be applied to any reducible subexpression of a larger overall expression.
|
3
|
|
conjunction
|
The "and" operator $A \land B$.
|
|
|
cons
|
The non-empty list, consisting of a head element and a tail list
|
1
|
|
constraint-based type inference
|
A method of type inference that casts the problem in constraint-satisfaction terms.
|
8
|
|
constructive
|
A property of a logic or proof that indicates it does not make use of the law of the excluded middle.
|
|
|
context
|
Usually written $\Gamma$, indicates a set of judgements that are assumed in a derivation. In type systems, usually is a mapping from variable name to type. Also can refer to an environment in dynamic semantics. Can be viewed as hypothetical derivation.
|
3
|
|
contradiction
|
The simultaneous derivation of both $A$ and $\neg A$.
|
|
|
contravariant
|
For a type constructor $C$, the variance where $\tau \leq \rho$ implies that $C\ \tau \geq C\ \rho$.
|
9
|
|
control structure
|
A syntactic construct to encapsulate some common pattern of control flow in an imperative language, such as a while loop or an if statement.
|
4
|
|
cost model
|
A type of dynamic semantics where the goal is not to describe the actual run-time behaviour (e.g. results returned) but instead to mathematically describe the computational resources used (e.g. for computational complexity) .
|
1
5
|
|
covariant
|
For a type constructor $C$, the variance where $\tau \leq \rho$ implies $C \tau \leq C \rho$.
|
9
|
|
critical section
|
A sequence of steps guaranteed to execute atomically due to various means of synchronisation.
|
10
|
|
Curry-Howard correspondence
|
The correspondence between programs and proofs, types and propositions, and evaluation to proof simplification.
|
7
|
|
identifier
|
An alphabetical (or alphanumeric) lexeme in a language's syntax, which could stand for e.g. a variable, function or type name.
|
1
|
|
if and only if
|
$A$ if and only if $B$ is the same as $(A \Rightarrow B) \land (B \Rightarrow A)$.
|
|
|
imperative programming
|
Where programs are described as a
series of statements or commands which manipulate mutable state or
cause externally observable effects
|
4
|
|
implication
|
The "if-then" operator $A \Rightarrow B$. Sometimes written $A \supset B$. It holds unless $A$ is true and $B$ is false.
|
|
|
implicitly-typed
|
Describes a language with no type annotations.
|
8
|
|
inconsistent
|
A logic that allows both $P$ and $\neg P$ to be proven for some $P$.
|
|
|
induction
|
A process of proof whereby a property is shown for elemental base cases, and then, assuming premises called inductive hypotheses, the property is shown for inductive cases, thereby proving the property for all of an inductive set.
|
2
|
|
inductive case
|
A proof case that is derived from a (non-axiom) inference rule in an inductive proof, with one or more inductive hypotheses taken as assumptions.
|
2
|
|
inductive definition
|
A set of inference rules that is describes a language or judgement completely. That is, the rules prove the judgement, and if the judgement holds then it must be via one of those rules.
|
2
|
|
inductive hypothesis
|
An assumption derived from a premise of the inference rule for a particular inductive cases of an inductive proof.
|
2
|
|
inference rule
|
A rule, written $\frac{J_1 \quad J_2 \quad \dots \quad J_n}{J}$, which states that in order to prove judgement $J$,
it suffices to prove judgements $J_1$ through to $J_n$.
|
2
|
|
inhabitant
|
A value $v$ is an inhabitant of a type $\tau$ if $v : \tau$.
|
7
|
|
initial state
|
The states in which a state machine may begin execution.
|
3
|
|
initialized
|
A property of a mutable variable that indicates it has been assigned a value after being declared.
|
4
|
|
injective
|
A mapping from set $A$ to set $B$ is injective if each different element in $A$ has a different corresponding element in $B$.
|
|
|
inlining
|
The optimisation that removes costly jumps by copying the code from a function into its call sites.
|
|
|
instance constraint
|
A constraint on a type that a type class must have a class instance.
|
9
|
|
instantiation
|
The substitution of a type variable to a concrete type.
|
8
|
|
integer
|
A whole number: positive, zero or negative.
|
|
|
interference
|
The actions of one process altering the results or execution of another process.
|
10
|
|
intermediate representation
|
A language used internally within a compiler or interpreter to make certain manipulations or optimisations simpler.
|
1
|
|
interpreter
|
A program which directly executes a program from source code given as input.
|
1
|
|
intersection
|
The intersection of sets $A \cap B$ is the set of elements common to both $A$ and $B$.
|
|
|
introduction
|
The inference rule in a logic that allows a logical operator to be introduced to the proven formula. Analogous
to a data constructor in a programming language.
|
2
|
|
invariant
|
A variance which is neither covariant nor contravariant.
|
9
|
|
irreducible
|
A term is irreducible if no reduction may be applied to it.
|
3
|
|
isolation
|
A property of a process in a concurrent application where it is as though the process is executed in isolation --- its effects should not be themselves affected by other threads.
|
10
|
|
isomorphic
|
Two types are isomorphic, written $\tau_1 \simeq \tau_2$, if and only if there exists a bijection between them. Typically, this is if they have the same number of inhabitants.
|
7
|
|
M-machine
|
The small-step semantics of MinHS, as an abstract machine.
|
5
|
|
maximal
|
A trace or execution $\sigma_1 \dots \sigma_n$ is maximal if and only if there is no $\sigma_{n+1}$ such that the $\sigma_n \mapsto \sigma_{n+1}$ according to the transition relation.
|
3
|
|
meta-language
|
The language within which another language is described. In this course, we use Haskell as a meta-language in the assignments, and a meta-logic as our meta-language in the mathematical work.
|
2
|
|
meta-logic
|
A bare-bones logical system designed to specify another logic or programming language. In this course we use Natural Deduction.
|
2
|
|
method
|
An overloaded variable name that must be implemented to create a class instance of a type class.
|
9
|
|
mgu
|
most general unifier.
|
8
|
|
MinHS
|
A minimal functional programming language (that is purely functional) we specified in Week 5.
|
4
|
|
module
|
A value encapsulating an abstract data type, i.e. an existential type.
|
9
|
|
modus ponens
|
The argument that if $A \Rightarrow B$ and $A$, then $B$. Also called implication elimination.
|
|
|
modus tollens
|
The argument that if $A \Rightarrow B$ and $\neg B$, then $\neg A$.
|
|
|
monad
|
A convenient abstraction in Haskell, allows for the simulation of mutable state, exceptions and much more.
|
7
9
|
|
monomorphic
|
Refers to something that is not polymorphic.
|
8
|
|
more general
|
A type $\tau$ is more general than a type $\rho$, written $\rho \sqsubset \tau$, if a substitution can be made to polymorphic type variables in $\tau$ to give $\rho$.
|
8
|
|
most general unifier
|
A unifier $S$ is most general for types $\tau$ and $\rho$ iff $S(\tau) = S(\rho)$ is the most general type that could result from unification.
|
8
|
|
mutable
|
An adjective that indicates that it may change over time, e.g. in the course of an execution.
|
4
9
|
|
mutual exclusion
|
The safety property that says that no two processes are in their critical section simultaneously.
|
10
|
|
parallelism
|
The simultaneous execution of code on multiple processors or cores for the purposes of improved performance.
|
9
|
|
parametric polymorphism
|
A feature of a language which allows functions to be defined operating on arbitrary types using type abstraction and type application. Sometimes called generics in Java.
|
8
|
|
parametricity
|
See relational parametricity.
|
8
|
|
parse tree
|
A tree that contains a representation of the grammatical structure recognized for a particular program by the parser. Often this is the same as the abstract syntax tree.
|
1
2
|
|
parser
|
The second phase of a compiler or interpreter which converts the sequence of tokens from the lexer to a parse tree according to the grammar rules of the language's syntax.
|
1
2
|
|
parsing
|
The relation $\longleftrightarrow$ that relates concrete to abstract syntax.
|
2
|
|
partial correctness
|
The property that says if a program evaluates from an initial state which satisfies the precondition, then any final state it reaches will satisfy the postcondition. As opposed to total correctness which requires that a final state is reached.
|
4
|
|
partial function
|
A function that is not defined for its whole domain.
|
|
|
partial order
|
A relation that is reflexive, transitive, and antisymmetric.
|
|
|
pessimistic
|
A property of a synchronisation model where interference is pre-emptively prevented before transactions are executed, such as locks. As opposed to optimistic models like transactional memory.
|
10
|
|
polymorphic recursion
|
A recursive, polymorphic program that calls itself with different type arguments on each recursive call.
|
8
|
|
polymorphism
|
Usually refers to parametric polymorphism, unless otherwise indicated.
|
8
9
|
|
postcondition
|
An assertion that will be satisfied by a program's final state if the precondition held for the initial state.
|
4
|
|
precondition
|
An assertion that must be satisfied by the initial state in order for the program's specification to apply.
|
4
|
|
predicate
|
A logical property that is parameterised by a mathematical object. Equivalently a function from some set to booleans.
|
|
|
premise
|
A judgement that must be proven in order to prove the conclusion of an inference rule.
|
2
|
|
preservation
|
A lemma needed to prove type safety which states that if a program $e$ has type $\tau$, i.e. $e : \tau$, and $e$ takes a step to $e'$, then $e' : \tau$.
|
7
|
|
pretty-printing
|
A process to transform abstract syntax back into concrete syntax by going right to left on the parsing relation.
|
2
|
|
process
|
A sequence of statements to execute that forms one thread of control in a concurrent application.
|
9
10
|
|
product type
|
A product type, written $\tau_1 \times \tau_2$, denotes the type of pairs or tuples of values of type $\tau_1$ and of $\tau_2$ respectively. Analogous to the cartesian product in set theory, and to conjunction via the Curry-Howard correspondence.
|
7
|
|
production
|
A syntax production describes how to recognize a non-terminal as a sequence of terminals and other non-terminals.
|
1
|
|
progress
|
The lemma that if an expression $e$ has type $\tau$, i.e. $e : \tau$ then either $e$ is a final state or $e$ can take a step to some state $e'$. Proves type safety along with preservation.
|
7
|
|
proof assistant
|
A tool for interactively proving theorems in a formal logic, such as Isabelle, Coq, or Agda.
|
|
|
proof by contradiction
|
The process of proof whereby the proof obligation is assumed to be false, and a contradiction is derived. Depends on excluded middle.
|
|
|
proof calculus
|
A set of inference rules to describe a logic or reasoning system.
|
2
4
|
|
proof obligation
|
A judgement that we wish to prove, or must prove in order to establish our ultimate proof goal.
|
|
|
property
|
A set of a program's behaviours. Often informally described as an English statement about a program's behaviour.
|
7
|
|
proposition
|
A logical statement. See judgement.
|
|
|
purely functional
|
A programming language is purely functional if β-reduction (or
evaluation in general) is actually a confluence.
In other words, functions have to be mathematical functions, and
free of side effects.
|
4
|
|
s-expressions
|
A particular type of term language where terms are either identifiers or parenthesised compounds consisting of one or more subterms.
|
2
|
|
safety
|
A type of property that states that something bad will not happen. Can be refuted by a finite prefix of a behaviour. For example, type safety, partial correctness.
|
7
|
|
scheduler
|
The operating system component that chooses which processes get to run.
|
10
|
|
schematic variable
|
See unification variable.
|
8
|
|
scope
|
The (sub)-expressions in which a variable is bound.
|
2
|
|
scope checking
|
See scope resolution.
|
1
2
|
|
scope resolution
|
The process by which variables and other references in a program are checked to see if they refer to objects that have been defined previously. Finds the correct binding occurrence for each usage occurrence of a variable.
|
1
2
|
|
second-order logic
|
A form of logic where quantifiers range over propositions that can themselves include quantifiers.
|
8
|
|
semantic analyser
|
The third phase of a compiler or interpreter which performs analysis on the abstract syntax tree to determine the static semantics of the input program.
|
1
|
|
semantics
|
The mathematical meaning of a program, in the form of dynamic semantics or static semantics.
|
1
3
|
|
sequential composition
|
A fancy term for the semicolon operator in TinyImp, i.e. $s_1 ; s_2$ which runs $s_2$ after $s_1$.
|
4
|
|
shadowing
|
The situation where a variable that is already in scope is bound. For example let x = 5 in let x = 2 in x + x end end.
|
2
|
|
shared variable
|
A mutable variable that may be accessed by multiple processes.
|
10
|
|
side effects
|
Side effects refers to effects that are not tracked by the type system.
|
4
|
|
signature
|
The type of a module.
|
9
|
|
simulation
|
A proof process to show refinement whereby each step taken by the concrete semantics can be matched by a step in the abstract semantics.
|
5
|
|
simultaneous induction
|
The process of treating multiple judgements as part of one large inductive definition for the purposes of induction.
|
2
3
|
|
small-step semantics
|
A means of specifying a language's dynamic semantics as the execution of a state machine, consisting of a set of initial states $I \subseteq \Sigma$, a set of final states $F \subseteq \Sigma$, and a transition relation $\mapsto \subseteq \Sigma \times \Sigma$ from state to state.
|
3
|
|
software transactional memory
|
A software-only implementation of transactional memory.
|
10
|
|
source code
|
The code written by the programmer in their text editor.
|
1
|
|
specification
|
A mathematical description of the desired properties of a program or software system.
|
|
|
stack
|
A list-like data structure which consists of an operation to push on items, and pop items off, in Last-In-First-Out order.
|
2
5
|
|
starvation
|
The scenario where a process is repeatedly denied entry into its critical section because of the scheduler's favouritism to other processes.
|
10
|
|
starvation-freedom
|
The property that starvation cannot occur. Used synonymously with eventual entry.
|
10
|
|
state
|
All the information required to evaluate a program at one step in its execution. For example, would include the values of all variables.
|
3
|
|
state machine
|
A mathematical formalism consisting of a set of states $\Sigma$, sets of initial and final states $I$ and $F$, and a transition relation $\mapsto \subseteq \Sigma \times \Sigma$.
|
3
|
|
static
|
Refers to properties or behaviour of programs that can be determined without running them, for example at compile-time.
|
1
|
|
static semantics
|
Mathematical description of the aspects of a program that can be determined statically.
|
1
3
|
|
strict evaluation
|
See call-by-value.
|
3
|
|
strict subset
|
A set $A$ is a strict subset of a set $B$, written $A \subset B$, if $A$ is a subset of $B$ which is also not equal to $B$.
|
|
|
strict superset
|
A set $A$ is a strict superset of another set $B$ if $B$ is a strict subset of $A$.
|
|
|
strong normalisation
|
A property of typed λ-calculus that states that any expression will reduce to a normal form in finite time. This makes typed λ-calculus not Turing-complete, but suitable for a foundation for logic.
|
7
|
|
structural induction
|
A form of rule induction where the rules being used define the structure (type) of a particular variable.
|
2
|
|
structural operational semantics
|
See small-step semantics.
|
3
|
|
structured programming
|
A movement in the 1970s, headed by Edsger Dijkstra, to promote the use of control structures to aid in formal reasoning, in particular things like Hoare logic.
|
4
|
|
stuck state
|
A state that is not a final state but has no outgoing transitions in the transition relation.
|
7
|
|
subject reduction
|
A property of typed λ-calculus that states that the normal form of a term will have the same type as that term.
|
7
|
|
subset
|
A set $A$ is a subset of a set $B$, written $A \subseteq B$ if every element of $A$ is also an element of $B$.
|
|
|
substitution
|
Written $e[x:=t]$ or $e[{}^t/_x]$, means the replacement of all free usage occurrences of $x$ with $t$ in $e$.
|
2
|
|
subtyping
|
A partial order on types, written $\tau \leq \rho$. Always includes a
rule of subsumption in the type system.
|
9
|
|
sum type
|
The sum type, written $\tau_1 + \tau_2$, denotes either a value of type $\tau_1$ or a value of type $\tau_2$, distinguished by a data constructor. Analogous to disjunction in logic via the Curry-Howard correspondence, the disjoint union in set theory, or the Either type in Haskell.
|
7
|
|
superset
|
$A$ is a superset of $B$ if and only if $B$ is a subset of $A$.
|
|
|
surjective
|
A mapping from set $A$ to set $B$ is surjective if each element of $B$ has some element of $A$ that maps to it.
|
|
|
symmetric
|
A property of a relation $R$ where $a\ R\ b$ implies $b\ R\ a$ for all $a$ and $b$.
|
|
|
synchronisation
|
Where multiple processes co-ordinate or communicate to give predictable outcomes.
|
9
10
|
|
syntax
|
The rules of the language that describe how the language is written (e.g. according to a grammar), rather than what it means (semantics).
|
1
2
2
|
|
syntax-directed
|
When a set of inference rules can correspond to an algorithm by following the structure of abstract syntax.
|
8
|
|
tail
|
The rest of a non-empty list after the head.
|
1
|
|
tautology
|
A logical property that is self-evidently true, for example $A \Rightarrow A$.
|
|
|
template instantiation
|
A means of compiling polymorphic programs by statically generating a monomorphic copy of each polymorphic function.
|
8
|
|
term
|
An expression in a minimal language used in the meta-logic to describe syntax trees. Can also be used
in general to mean expression.
|
2
|
|
terminal
|
A raw lexeme that is is recognised as-is in a language's grammar.
|
1
|
|
termination
|
A property that states that a program halts in a final state after a finite amount of steps, i.e. that all maximal traces are finite completed traces.
|
3
|
|
theorem
|
A judgement or proposition that has been proven.
|
2
|
|
thread
|
See process.
|
9
10
|
|
throw
|
See raise.
|
7
|
|
TinyImp
|
An imperative programming language we specify in Week 5.
|
4
|
|
token
|
A single "word" in a programming language's syntax, e.g. a keyword, an identifier, or a literal. Also called a lexeme.
|
1
|
|
total correctness
|
The combination of partial correctness and termination.
|
4
|
|
trace
|
See execution.
|
3
|
|
transaction
|
See critical section. Used in the context of transactional memory.
|
10
|
|
transactional memory
|
An optimistic means of synchronisation where transactional variables are modified locally in a log, and then commited to shared variables only after validating to ensure the results are not inconsistent due to interference.
|
10
|
|
transactional variable
|
A special type of mutable variable where modifications are tracked using transactional memory.
|
10
|
|
transition relation
|
The relation $\mapsto$ in small-step semantics.
|
3
|
|
transition system
|
See state machine.
|
3
|
|
transitive
|
A property of a relation $R$ where $a\ R\ b$ and $b\ R\ c$ implies $a\ R\ c$ for all $a$, $b$, and $c$.
|
|
|
Turing-complete
|
A property of a language that means that it is capable of performing any decidable computation in finite time.
|
|
|
type
|
A type is a static tag that classifies expressions according to the sort of values they will evaluate to.
|
1
7
|
|
type abstraction
|
Written $\textbf{type}\ a. e$, indicates that the expression $e$ is parameterised by a type variable $a$.
|
8
|
|
type annotation
|
Some means of syntax for the programmer to specify types.
|
8
|
|
type application
|
Written $e@\tau$, instantiates the type variable in the type of $e$ to $\tau$.
|
8
|
|
type checking
|
The process by which the semantic analyser of a compiler establishes that a program is well-typed (or not!).
|
1
7
|
|
type class
|
A set of types that have provided implementations (class instances) for a set of overloaded functions (methods).
|
9
|
|
type constructor
|
A type with a hole in it for a parameter. For example, $\mathtt{Maybe}\ \square$ or $\square \rightarrow \mathtt{Int}$.
|
9
|
|
type inference
|
The process of determining what type would make an expression well-typed, given an implicitly-typed language.
|
8
|
|
type safety
|
The safety property that states that well-typed programs do not reach a stuck state. Usually proven via progress and preservation.
|
7
|
|
type system
|
A formal scheme of assigning types to expressions.
|
7
|
|
type theory
|
A logic based on typed λ-calculus and the Curry-Howard correspondence, used as the foundation for many constructive proof assistants.
|
3
7
|
|
type variable
|
A variable that stands for a type, usually in the context of parametric polymorphism.
|
8
|
|
typed λ-calculus
|
A variant of λ-calculus with a type system. Is not Turing-complete but enjoys strong normalisation and subject reduction.
|
7
|