ОБ ЭТОМ ЭПИЗОДЕ
Discussion of the connection between normalization and logical consistency. One approach is to prove normalization and type preservation, to show (in proof-theoretic terms) that all detours can be eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation). I mention an alternative I use for Cedille, which is to use a realizability semantics (often used for normalization proofs) directly to prove consistency.
английский
США
В ЭТОМ ЭПИЗОДЕ
РАСШИФРОВКА 🔗
Are you the producer of this podcast?
Add a podcast transcript
Need Audio-to-Text?
Transcribe with Listen411 in Just 60 Seconds
ПОИСК ПРОШЛЫХ ЭПИЗОДОВ
Искать прошлые эпизоды Iowa Type Theory Commute.
ДРУГИЕ ЭПИЗОДЫ В ЭТОМ ПОДКАсте
I am currently on a frolic into the literature on Control Flow Analysis (CFA), and discuss what this is, for pure lambda calculus. A wonderful reference for this is this paper by Palsberg.
I discuss a nice paper I quite enjoyed reading, called The Calculated Typer, by Garby, Bahr, and Hutton. The authors take a very nice general look at the specification of a type checker, for a very simple expression language. They then manually derive the actual code for the type checker by effec…
In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connection between logic and programming languages where formulas in logic are identified with types, and proofs with programs). This is the identification of double-negation translations in logic, whi…
In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CPS). I sketch how CPS conversion (transforming a program with callcc into one in CPS that does not need callcc any more) corresponds to double-negation transla…
Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour reductions (which correspond to beta-reduction under Curry-Howard) are enabled. The stuck inferences are uses of disjunction elimination. In progr…
Отказ от ответственности: Подкаст и иллюстрации, встроенные в эту страницу, взяты из Aaron Stump, который является собственностью его владельца и не связан или не одобрен Listen Notes, Inc.
ИЗМЕНИТЬ
Спасибо, что помогаете поддерживать базу подкастов актуальной.
