The following pages link to LEGO (Q21664):
Displaying 50 items.
- Unifying sets and programs via dependent types (Q408534) (← links)
- Alpha equivalence equalities (Q428860) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694) (← links)
- Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
- Dependently typed records in type theory (Q699688) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- A compact kernel for the calculus of inductive constructions (Q1040007) (← links)
- Type checking with universes (Q1177937) (← links)
- Metacircularity in the polymorphic \(\lambda\)-calculus (Q1177938) (← links)
- The extended calculus of constructions (ECC) with inductive types (Q1193601) (← links)
- Verifying programs in the calculus of inductive constructions (Q1267035) (← links)
- Simply-typed underdeterminism (Q1273067) (← links)
- Order-sorted inductive types (Q1286367) (← links)
- On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations (Q1302298) (← links)
- Inductive families (Q1336951) (← links)
- An overview of the Tecton proof system (Q1341710) (← links)
- Categorical abstract machines for higher-order typed \(\lambda\)-calculi (Q1349667) (← links)
- Indexed types (Q1389626) (← links)
- Search algorithms in type theory (Q1575934) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- \(\pi\)-calculus in (Co)inductive-type theory (Q1589654) (← links)
- Proof planning for strategy development (Q1601860) (← links)
- Autarkic computations in formal proofs (Q1610674) (← links)
- Transitivity in coercive subtyping (Q1776403) (← links)
- An experiment concerning mathematical proofs on computers with French undergraduate students (Q1884267) (← links)
- Kinded type inference for parametric overloading (Q1911131) (← links)
- The locally nameless representation (Q1945914) (← links)
- Special issue: Formal proof (Q1961912) (← links)
- Some lambda calculus and type theory formalized (Q1961921) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- Dealing with algebraic expressions over a field in Coq using Maple (Q2456560) (← links)
- A higher-order calculus and theory abstraction (Q2639838) (← links)
- (Q2723890) (← links)
- (Q2729065) (← links)
- (Q2754063) (← links)
- Generation and presentation of formal mathematical documents (Q2760868) (← links)
- (Q2769425) (← links)
- Type theory should eat itself (Q2804938) (← links)
- Comparing higher-order encodings in logical frameworks and tile logic (Q2841275) (← links)
- Constructive membership predicates as index types (Q2866329) (← links)
- Type-level computation using narrowing in \(\Omega\)mega (Q2866338) (← links)
- Normalization for the simply-typed lambda-calculus in Twelf (Q2871835) (← links)
- A language-based approach to functionally correct imperative programming (Q2936790) (← links)
- Unifiers as equivalences: proof-relevant unification of dependently typed data (Q2985776) (← links)
- A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems (Q3003307) (← links)
