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 |