Cited in
(only showing first 100 items - show all)- A compact kernel for the calculus of inductive constructions
- Proof assistants: history, ideas and future
- scientific article; zbMATH DE number 1424053 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Two case studies of semantics execution in Maude: CCS and LOTOS
- Artificial Intelligence and Symbolic Computation
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- Proof planning for strategy development
- scientific article; zbMATH DE number 1512607 (Why is no real title available?)
- An overview of the Tecton proof system
- The locally nameless representation
- Equations: a dependent pattern-matching compiler
- Alpha equivalence equalities
- scientific article; zbMATH DE number 1231611 (Why is no real title available?)
- Functional and Logic Programming
- scientific article; zbMATH DE number 1301731 (Why is no real title available?)
- Some lambda calculus and type theory formalized
- scientific article; zbMATH DE number 2085175 (Why is no real title available?)
- The practice of logical frameworks
- Theorem Proving in Higher Order Logics
- Proof by computation in the Coq system
- Exploring abstract algebra in constructive type theory
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Ynot: dependent types for imperative programs
- Lolli
- scientific article; zbMATH DE number 1863382 (Why is no real title available?)
- Inductive families
- A language-based approach to functionally correct imperative programming
- Program specification and data refinement in type theory
- Unifying sets and programs via dependent types
- A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits
- Indexed types
- Autarkic computations in formal proofs
- Internal type theory
- scientific article; zbMATH DE number 1420791 (Why is no real title available?)
- The extended calculus of constructions (ECC) with inductive types
- scientific article; zbMATH DE number 1927413 (Why is no real title available?)
- \(\pi\)-calculus in (Co)inductive-type theory
- Coq
- HYBRID
- ML
- Verifying programs in the calculus of inductive constructions
- Nuprl
- Automath
- Plastic
- The seven virtues of simple type theory
- AURA
- scientific article; zbMATH DE number 1420782 (Why is no real title available?)
- ALF
- Cayenne
- Epigram
- Minlog
- CtCoq
- PoplMark
- Analytica
- SAFL
- LOTOSphere
- Ivor, a Proof Engine
- A natural deduction approach to dynamic logic
- scientific article; zbMATH DE number 1005001 (Why is no real title available?)
- Termination checking with types
- XBarnacle
- Elf
- mini-ML
- TIL
- SKIL
- Gallina
- AFFIRM
- Tecton
- Cambridge LCF
- A Normalizing Intuitionistic Set Theory with Inaccessible Sets
- scientific article; zbMATH DE number 1301735 (Why is no real title available?)
- scientific article; zbMATH DE number 591911 (Why is no real title available?)
- Order-sorted inductive types
- On the role of OpenMath in interactive mathematical documents
- Using typed lambda calculus to implement formal systems on a machine
- scientific article; zbMATH DE number 1629953 (Why is no real title available?)
- Dependently typed records in type theory
- scientific article; zbMATH DE number 1670760 (Why is no real title available?)
- A canonical locally named representation of binding
- Mathematical Knowledge Management
- scientific article; zbMATH DE number 512769 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- Search algorithms in type theory
- Coercion completion and conservativity in coercive subtyping
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- Type-level computation using narrowing in \(\Omega\)mega
- Kinded type inference for parametric overloading
- A partial type checking algorithm for Type:Type
- Constructive membership predicates as index types
- scientific article; zbMATH DE number 1231700 (Why is no real title available?)
- A Dependently Typed Framework for Static Analysis of Program Execution Costs
- Transitivity in coercive subtyping
- A higher-order calculus and theory abstraction
- scientific article; zbMATH DE number 2242593 (Why is no real title available?)
- More Church-Rosser proofs (in Isabelle/HOL)
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- ProofWidgets
- Structural subtyping for inductive types with functorial equality rules
This page was built for software: LEGO
