scientific article; zbMATH DE number 512790
From MaRDI portal
Publication:4281483
Cited in
(83)- Order-sorted inductive types
- Synthesis of ML programs in the system Coq
- Inductive families
- Formalizing process algebraic verifications in the calculus of constructions
- Abstract data type systems
- Induction-recursion and initial algebras.
- Formalizing mathematics in higher-order logic: A case study in geometric modelling
- Cut-elimination for a logic with definitions and induction
- -calculus in (Co)inductive-type theory
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- Transitivity in coercive subtyping
- On the formalization of the modal -calculus in the calculus of inductive constructions
- Finitary higher inductive types in the groupoid model
- Parametric Church's thesis: synthetic computability without choice
- Constructive and mechanised meta-theory of intuitionistic epistemic logic
- Indexed induction-recursion
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Developing (meta)theory of -calculus in the theory of contexts
- Certifying term rewriting proofs in ELAN
- The theory of contexts for first order and higher order abstract syntax
- Inductive and coinductive components of corecursive functions in Coq
- Deciding regular expressions (in-)equivalence in Coq
- Notions of anonymous existence in Martin-Löf type theory
- scientific article; zbMATH DE number 4014064 (Why is no real title available?)
- scientific article; zbMATH DE number 7037626 (Why is no real title available?)
- Practical Tactics for Separation Logic
- Structural subtyping for inductive types with functorial equality rules
- A Short Presentation of Coq
- Dual Calculus with Inductive and Coinductive Types
- Lexicographic Path Induction
- A New Elimination Rule for the Calculus of Inductive Constructions
- Formal specification and proofs for the topology and classification of combinatorial surfaces
- scientific article; zbMATH DE number 1223720 (Why is no real title available?)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- On lists and other abstract data types in the calculus of constructions
- ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS
- Modular properties of algebraic type systems
- Automating inversion of inductive predicates in Coq
- An application of co-inductive types in Coq: verification of the alternating bit protocol
- Proof normalization modulo
- Remarks on isomorphisms of simple inductive types
- A syntax for higher inductive-inductive types
- Cumulative inductive types in Coq
- The Interpretation Lifting Theorem for C-Systems
- Practical Proof Search for Coq by Type Inhabitation
- Encoding natural semantics in Coq
- A fixedpoint approach to implementing (co)inductive definitions
- Signatures and induction principles for higher inductive-inductive types
- Program testing and the meaning explanations of intuitionistic type theory
- Eliminating dependent pattern matching without K
- Experimenting Formal Proofs of Petri Nets Refinements
- Types for Proofs and Programs
- Compositional coinduction with sized types
- A case-study in algebraic manipulation using mechanized reasoning tools
- Least and greatest fixed points in intuitionistic natural deduction
- Primitive recursion for higher-order abstract syntax
- Formalization of a λ-calculus with explicit substitutions in Coq
- Developing certified programs in the system Coq the program tactic
- Codifying guarded definitions with recursive schemes
- An automatically verified prototype of the Android permissions system
- Material dialogues for first-order logic in constructive type theory
- Formal Verification of Bit-Vector Invertibility Conditions in Coq
- Congruence types
- An analysis of Tennenbaum's theorem in constructive type theory
- Topological quantum gates in homotopy type theory
- Theoretical computer science: computability, decidability and logic
- Material dialogues for first-order logic in constructive type theory: extended version
- A type checker for a logical framework with union and intersection types (system description)
- A syntax for mutual inductive families
- The Kleene-Post and Post's theorem in the calculus of inductive constructions
- Consistent ultrafinitist logic
- On systems of definitions, induction and recursion
- An introduction to mathematical formalization based on lean
- A weakly initial algebra for higher-order abstract syntax in Cedille
- Touring the MetaCoq project
- Completeness of first-order bi-intuitionistic logic
- Reflexive graph lenses in univalent foundations
- Inductive predicates via least fixpoints in higher-order separation logic
- A two-level linear dependent type theory
- Dynamic Pushdown Networks
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
- Gödel's system T revisited
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4281483)
