Analysis and synthesis of inductive families
<p>Based on a natural unification of logic and computation, Martin-Löf’s <em>intuitionistic type theory</em> can be regarded simultaneously as a computationally meaningful higher-order logic system and an expressively typed functional programming language, in which proofs and progr...
| Egile nagusia: | |
|---|---|
| Beste egile batzuk: | |
| Formatua: | Thesis |
| Hizkuntza: | English |
| Argitaratua: |
2014
|