scientific article; zbMATH DE number 512790
From MaRDI portal
Publication:4281483
zbMath0844.68073MaRDI QIDQ4281483
Publication date: 10 March 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Unnamed Item ⋮ Finitary higher inductive types in the groupoid model ⋮ Inductive families ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps ⋮ Practical Tactics for Separation Logic ⋮ Formalizing process algebraic verifications in the calculus of constructions ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ Deciding Regular Expressions (In-)Equivalence in Coq ⋮ Design and formal proof of a new optimal image segmentation program with hypermaps ⋮ Unnamed Item ⋮ Encoding natural semantics in Coq ⋮ Abstract data type systems ⋮ Formal specification and proofs for the topology and classification of combinatorial surfaces ⋮ 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 ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Material dialogues for first-order logic in constructive type theory ⋮ Induction-recursion and initial algebras. ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Eliminating dependent pattern matching without K ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof ⋮ Experimenting Formal Proofs of Petri Nets Refinements ⋮ 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 ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Compositional Coinduction with Sized Types ⋮ Remarks on Isomorphisms of Simple Inductive Types ⋮ A case-study in algebraic manipulation using mechanized reasoning tools ⋮ Transitivity in coercive subtyping ⋮ Least and greatest fixed points in intuitionistic natural deduction ⋮ Primitive recursion for higher-order abstract syntax ⋮ A fixedpoint approach to implementing (Co)inductive definitions ⋮ Dual Calculus with Inductive and Coinductive Types ⋮ Lexicographic Path Induction ⋮ A New Elimination Rule for the Calculus of Inductive Constructions ⋮ Order-sorted inductive types ⋮ Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. ⋮ Certifying Term Rewriting Proofs in ELAN ⋮ The Theory of Contexts for First Order and Higher Order Abstract Syntax ⋮ Formalizing mathematics in higher-order logic: A case study in geometric modelling ⋮ Cut-elimination for a logic with definitions and induction ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ \(\pi\)-calculus in (Co)inductive-type theory ⋮ Indexed induction-recursion ⋮ On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq ⋮ Synthesis of ML programs in the system Coq
Uses Software
