Deduction in Ramified Partial Type Theory: Focus on Derivation with Typing Judgements
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F16%3A00113939" target="_blank" >RIV/00216224:14210/16:00113939 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Deduction in Ramified Partial Type Theory: Focus on Derivation with Typing Judgements
Original language description
In computer science, type theory is massively used as the basis of functional programming and theorem provers. Explicit use of typing judgements, e.g. ``$X$ is of type $tau$.'', enables us a better control of programme behaviour (preventing cycling, ...), better control over quantification (preventing paradoxes, ...). The present talk focuses on deduction with typing judgements in Tichý's partial type theory, which is valuable because of its implementing partiality, incl. partiality of entities allowed in its ramified part.
Czech name
—
Czech description
—
Classification
Type
O - Miscellaneous
CEP classification
—
OECD FORD branch
60301 - Philosophy, History and Philosophy of science and technology
Result continuities
Project
<a href="/en/project/GA16-19395S" target="_blank" >GA16-19395S: Semantic notions, paradoxes and hyperintensional logic based on modern ramified theory of types</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů