TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
A | |
admissible rules | |
B | |
bi-intuitionistic logic | |
C | |
classical logic | |
Classical sequent calculus | |
Consistency proofs | |
Continuous computation | |
Curry-Howard | |
cut-elimination | |
cyclic induction | |
Cyclic proofs | |
D | |
denotational semantics | |
dualized proof system | |
E | |
expansion proofs | |
F | |
fibred category theory | |
first-order logic with inductive definitions | |
H | |
Herbrand's theorem | |
Higher order recursion schemes | |
I | |
induction reasoning | |
Infinite computation | |
Infinitely nested Boolean structure | |
Intuitionistic logic | |
Intuitionistic logic of constant domains | |
M | |
mechanical reasoning | |
mu-mutilde-calculus | |
N | |
Natural deduction | |
Non-wellfounded proofs | |
P | |
Peano arithmetic | |
proof terms | |
Proof theory | |
proofs-as-programs-as-morphisms | |
propositional logic | |
R | |
Reductive cut elimination | |
S | |
sequent calculus | |
T | |
Type reduction | |
Typed lambda-mu calculus |