LFMTP REGULAR PAPERS: KEYWORD INDEX

A | |

Abella | |

Abstract syntax | |

B | |

Barendregt's Variable Convention | |

binder mobility | |

Binders | |

C | |

computation and deduction | |

computational type theory | |

Constructive Type Theory | |

Coq | |

cubical type theory | |

D | |

Dedukti | |

E | |

exhaustive and randomized data generation | |

F | |

Formal Definition | |

Formal Metatheory | |

functional and relational specifications | |

functional programming | |

G | |

Generic Binding Structures | |

H | |

Higher-order abstract syntax (HOAS) | |

HOL | |

I | |

Interoperability | |

L | |

lambda calculus | |

lambda-tree syntax | |

Logical Frameworks | |

M | |

Matita | |

mechanized meta-theory | |

N | |

Notation | |

O | |

OCaml library | |

OpenTheory | |

P | |

proof assistant | |

property-based testing | |

R | |

refinement logic | |

S | |

Set Theory | |

T | |

two-level type theory | |

typed assembly languages |