Deduction in Ramified Partial Type Theory: Focus on Derivation with Typing Judgements

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Deduction in Ramified Partial Type Theory: Focus on Derivation with Typing Judgements

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Deduction in Ramified Partial Type Theory: Focus on Derivation with Typing Judgements

Popis výsledku anglicky

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.

Druh

O - Ostatní výsledky

CEP obor

—

OECD FORD obor

60301 - Philosophy, History and Philosophy of science and technology

Projekt

<a href="/cs/project/GA16-19395S" target="_blank" >GA16-19395S: Sémantické pojmy, paradoxy a hyperintenzionální logika založená na moderní rozvětvené teorii typů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů