The following pages link to Herman Geuvers (Q235622):
Displaying 50 items.
- The correctness of Newman's typability algorithm and some of its extensions (Q549191) (← links)
- Levels of undecidability in rewriting (Q627134) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- (Q1040000) (redirect page) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Explicit substitution. On the edge of strong normalization (Q1274458) (← links)
- A constructive algebraic hierarchy in Coq. (Q1404425) (← links)
- A formalisation of consistent consequence for Boolean equation systems (Q1687766) (← links)
- The \(\lambda \mu^{\mathbf{T}}\)-calculus (Q1946673) (← links)
- The construction of set-truncated higher inductive types (Q2133178) (← links)
- The Tactician. A seamless, interactive tactic learner and prover for Coq (Q2219409) (← links)
- Proof-assistants using dependent type systems (Q2751370) (← links)
- (Q2754042) (← links)
- Certified and portable mathematical documents from formal contexts (Q2767915) (← links)
- (Q2778821) (← links)
- Formal Mathematics on Display: A Wiki for Flyspeck (Q2843012) (← links)
- A calculus of tactics and its operational semantics (Q2847396) (← links)
- Deduction graphs with universal quantification (Q2870317) (← links)
- A logical framework with explicit conversions (Q2871837) (← links)
- Type theory and formal proof. An introduction (Q2925448) (← links)
- (Q2988060) (← links)
- Constructive analysis, types and exact real numbers (Q3431542) (← links)
- Proviola: A Tool for Proof Re-animation (Q3582730) (← links)
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype (Q3582731) (← links)
- (In)consistency of Extensions of Higher Order Logic and Type Theory (Q3612441) (← links)
- A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$ (Q3637295) (← links)
- Social processes, program verification and all that (Q3643359) (← links)
- Degrees of Undecidability in Term Rewriting (Q3644753) (← links)
- Modularity of strong normalization in the algebraic-λ-cube (Q4234771) (← links)
- (Q4362916) (← links)
- (Q4411846) (← links)
- Type Theory based on Dependent Inductive and Coinductive Types (Q4635888) (← links)
- Modular properties of algebraic type systems (Q4645803) (← links)
- (Q4703134) (← links)
- Some logical and syntactical observations concerning the first-order dependent type system λP (Q4704760) (← links)
- (Q4736391) (← links)
- (Q4736392) (← links)
- (Q4939698) (← links)
- (Q4945243) (← links)
- (Q4957790) (← links)
- (Q4995377) (← links)
- Characteristics of de Bruijn’s early proof checker Automath (Q5089679) (← links)
- (Q5155676) (← links)
- Introduction to Type Theory (Q5191087) (← links)
- Learning2Reason (Q5200132) (← links)
- Strong Normalization for Truth Table Natural Deduction (Q5212037) (← links)
- Deriving Natural Deduction Rules from Truth Tables (Q5224496) (← links)
- Natural deduction via graphs: formal definition and computation rules (Q5308097) (← links)
- Mathematical Knowledge Management (Q5313080) (← links)
- Communicating Formal Proofs: The Case of Flyspeck (Q5327363) (← links)
