The following pages link to (Q5753923):
Displayed 49 items.
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Impossibility of gathering, a certification (Q483063) (← links)
- Realizability models and implicit complexity (Q534712) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- On modal logics of partial recursive functions (Q817692) (← links)
- Formalizing non-interference for a simple bytecode language in Coq (Q931434) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Metacircularity in the polymorphic \(\lambda\)-calculus (Q1177938) (← links)
- The extended calculus of constructions (ECC) with inductive types (Q1193601) (← links)
- The undecidability of pattern matching in calculi where primitive recursive functions are representable (Q1208421) (← links)
- Synthesis of ML programs in the system Coq (Q1322847) (← links)
- Inductive families (Q1336951) (← links)
- Formalizing process algebraic verifications in the calculus of constructions (Q1355748) (← links)
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory (Q1392287) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice (Q1756495) (← links)
- Automata-driven automated induction (Q1854445) (← links)
- Certifying Findel derivatives for blockchain (Q2043802) (← links)
- Constructive hybrid games (Q2096468) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- Completeness and expressiveness of pointer program verification by separation logic (Q2417849) (← links)
- Logic of subtyping (Q2500487) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- A higher-order calculus and theory abstraction (Q2639838) (← links)
- Procedural representation of CIC proof terms (Q2655331) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- On Choice Rules in Dependent Type Theory (Q2988806) (← links)
- A Type-Theoretic Framework for Certified Model Transformations (Q2999313) (← links)
- A Short Presentation of Coq (Q3543643) (← links)
- Size-based termination of higher-order rewriting (Q4577817) (← links)
- Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
- (Q5015189) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis (Q5048989) (← links)
- Constructive sheaf models of type theory (Q5084309) (← links)
- Formal categorical reasoning (Q5102205) (← links)
- Computer Certified Efficient Exact Reals in Coq (Q5200110) (← links)
- Type Theories from Barendregt’s Cube for Theorem Provers (Q5251190) (← links)
- The calculus of dependent lambda eliminations (Q5372010) (← links)
- High-Level Theories (Q5505502) (← links)
- Synchronous gathering without multiplicity detection: a certified algorithm (Q5920218) (← links)
- Inductive-data-type systems (Q5958292) (← links)
- Least and greatest fixed points in intuitionistic natural deduction (Q5958300) (← links)
- The metatheory of UTT (Q6061874) (← links)
- (Q6068934) (← links)
- What is the point of computers? A question for pure mathematicians (Q6118162) (← links)