<!DOCTYPE html>
<html>
<head>
<title>Set Theory and Analysis</title>
</head>
<body>
<p>
Tuesday, 11 February 2025 - 10:00 to 11:30 <br />
Place: IM, konírna
</p>
<p>
Speaker: Tristan Bice, IM CAS<br />
Title: Dependent Type Semantics
</p>
<p class="ql-ed">
Abstract <br />
<p>Logical systems relying on dependent types underlie some of the most popular proof assistants these days such as Coq and Lean. While type theory is well known to computer scientists, there is scant material available to bridge the gap between the more classical logic familiar to most mathematicians. One barrier of entry is the lack of any clear semantics for type theory, with the meaning of the formalism usually given only in vague terms and often conflated with its syntax. This quickly leads to nonsensical statements like “in type theory, a proposition is the type of its proofs, which are all the same anyway, by proof-irrelevance”. Drawing from the speaker’s struggles in trying to get their head around these kinds of statements, we will give some simple but precise interpretations of dependent types, motivated by the semantics of classical propositional and predicate logic.</p>
</p>
<p>
For more information see the seminar web page at <br />
https://www.math.cas.cz/index.php/events/seminar/6
</p>
<p>
Set Theory and Analysis mailing list <br />
settfa@math.cas.cz <br />
https://list.math.cas.cz/listinfo/settfa@math.cas.cz
</p>
</body>
</html>