The following pages link to (Q4281483):
Displaying 50 items.
- Formal specification and proofs for the topology and classification of combinatorial surfaces (Q396466) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps (Q839032) (← links)
- Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof (Q944364) (← links)
- Gödel's system \(\mathcal T\) revisited (Q960861) (← links)
- Order-sorted inductive types (Q1286367) (← 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)
- Abstract data type systems (Q1391729) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Formalizing mathematics in higher-order logic: A case study in geometric modelling (Q1575663) (← links)
- Cut-elimination for a logic with definitions and induction (Q1575931) (← links)
- \(\pi\)-calculus in (Co)inductive-type theory (Q1589654) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- Transitivity in coercive subtyping (Q1776403) (← links)
- On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions (Q1854404) (← links)
- Finitary higher inductive types in the groupoid model (Q2130587) (← links)
- Parametric Church's thesis: synthetic computability without choice (Q2151397) (← links)
- Constructive and mechanised meta-theory of intuitionistic epistemic logic (Q2151399) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- Design and formal proof of a new optimal image segmentation program with hypermaps (Q2643883) (← links)
- Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts (Q2841233) (← links)
- Certifying term rewriting proofs in ELAN (Q2841249) (← links)
- The theory of contexts for first order and higher order abstract syntax (Q2841274) (← links)
- Inductive and coinductive components of corecursive functions in Coq (Q2873661) (← links)
- Deciding Regular Expressions (In-)Equivalence in Coq (Q2915138) (← links)
- Notions of anonymous existence in Martin-Löf type theory (Q2980980) (← links)
- (Q3121528) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- Structural subtyping for inductive types with functorial equality rules (Q3535679) (← links)
- Dual Calculus with Inductive and Coinductive Types (Q3636828) (← links)
- Lexicographic Path Induction (Q3637202) (← links)
- A New Elimination Rule for the Calculus of Inductive Constructions (Q3638245) (← links)
- ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS (Q4579809) (← links)
- Modular properties of algebraic type systems (Q4645803) (← links)
- Automating inversion of inductive predicates in Coq (Q4647573) (← links)
- An application of co-inductive types in Coq: Verification of the alternating bit protocol (Q4647576) (← links)
- Proof normalization modulo (Q4650285) (← links)
- Remarks on Isomorphisms of Simple Inductive Types (Q4924549) (← links)
- A Syntax for Higher Inductive-Inductive Types (Q4993350) (← links)
- The Interpretation Lifting Theorem for C-Systems (Q5025082) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- Encoding natural semantics in Coq (Q5096388) (← links)
- A fixedpoint approach to implementing (Co)inductive definitions (Q5210768) (← links)
- (Q5216301) (← links)
- Program Testing and the Meaning Explanations of Intuitionistic Type Theory (Q5253930) (← links)
- Eliminating dependent pattern matching without K (Q5371975) (← links)
- Experimenting Formal Proofs of Petri Nets Refinements (Q5403468) (← links)
- Compositional Coinduction with Sized Types (Q5739446) (← links)
