# nLab program

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## In type theory

In computer science a program is a construction of a term of a certain type (the output of the program).

Under computational trinitarianism this is essentially the same as a proof in type theory of the proposition presented by the type (see at propositions as types and proofs as programs).

Last revised on May 22, 2019 at 05:37:55. See the history of this page for a list of all contributions to it.