# Connexions

You are here: Home » Content » Propositional Logic: type checking

### Lenses

What is a lens?

#### Definition of a lens

##### Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

##### What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

##### Who can create a lens?

Any individual member, a community, or a respected organization.

##### What are tags?

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

#### Affiliated with (What does "Affiliated with" mean?)

This content is either by members of the organizations listed or about topics related to the organizations listed. Click each link to see a list of all content affiliated with the organization.
• Rice Digital Scholarship

This module is included in aLens by: Digital Scholarship at Rice UniversityAs a part of collection: "Intro to Logic"

Click the "Rice Digital Scholarship" link to see all content affiliated with them.

### Recently Viewed

This feature requires Javascript to be enabled.

# Propositional Logic: type checking

## Proofs and programming

Proofs are organized a lot like programs. Based on some premises (inputs), we obtain some conclusion (output) after using a series of inference rules (basic computation like addition and other operations). Using subproofs, especially when citing previous proofs, is just like organizing our program into functions that can be used many times.

Naturally, since using inference rules is not only how people prove things, but also computers. A clear example is in type checking. The core idea of type checking a function application is “If function f takes an argument of type αα and producing an output of type ββ, and expression exp is of type αα, then f(exp) is of type ββ.” This type rule closely resembles Elim: “If a proven formula is aba b and other proven formula is aa, then together, bb is a proven formula.” Furthermore, this similarity is highlighted by notation in many programming languages which would write the type of f as ααββ. Type rules are simply inference rules for proving results about the types of programs, and in most typical programming languages these rules closely correspond to those we are using for logic. This correspondence is known as the Curry-Howard Isomorphism.

As with logic, we want type checkers to be sound and complete. Soundness here means that if the program passes type checking, when we execute the program (or single function) and get a value, that value is of the stated type. In other words, if our program type checks, then we are guaranteed that some kinds of errors will not happen at run-time. That also means that if our program would have a run-time type error, the type checker will correctly report that our program is erroneous. Completeness here means that if we execute the program (or single function) and get a value of a certain type, then our type checker indeed tells us that type.

Note that type checking is still an area of active research, since the job is made difficult in the presence of language features such as inheritance, multiple inheritance, dynamic class loading, etc. When people introduce new computer languages with new features, and want to claim that their new language is type safe (that no function ever will be applied to the wrong type at run-time), then the paper which introduces the language will contain such a proof.

## Content actions

### Give feedback:

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

#### Definition of a lens

##### Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

##### What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

##### Who can create a lens?

Any individual member, a community, or a respected organization.

##### What are tags?

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

| External bookmarks