E-resources
-
Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro
Theoretical computer science, 07/2017, Volume: 685Journal Article
We develop metatheory of the Lambda calculus in Constructive Type Theory, using a first-order presentation with one sort of names for both free and bound variables and without identifying terms up to α-conversion. Concerning β-reduction, we prove the Church–Rosser theorem and the Subject Reduction theorem for the system of assignment of simple types. It is thereby shown that this concrete approach allows for gentle full formalisation, thanks to the use of an appropriate notion of substitution due to A. Stoughton. The whole development has been machine-checked using the system Agda.
Shelf entry
Permalink
- URL:
Impact factor
Access to the JCR database is permitted only to users from Slovenia. Your current IP address is not on the list of IP addresses with access permission, and authentication with the relevant AAI accout is required.
Year | Impact factor | Edition | Category | Classification | ||||
---|---|---|---|---|---|---|---|---|
JCR | SNIP | JCR | SNIP | JCR | SNIP | JCR | SNIP |
Select the library membership card:
If the library membership card is not in the list,
add a new one.
DRS, in which the journal is indexed
Database name | Field | Year |
---|
Links to authors' personal bibliographies | Links to information on researchers in the SICRIS system |
---|
Source: Personal bibliographies
and: SICRIS
The material is available in full text. If you wish to order the material anyway, click the Continue button.