Cited in
(only showing first 100 items - show all)- A partial type checking algorithm for Type:Type
- Artificial Intelligence and Symbolic Computation
- scientific article; zbMATH DE number 2090315 (Why is no real title available?)
- Autarkic computations in formal proofs
- Metacircularity in the polymorphic \(\lambda\)-calculus
- Type checking with universes
- Types for Proofs and Programs
- Theorem Proving in Higher Order Logics
- scientific article; zbMATH DE number 2242593 (Why is no real title available?)
- Type theoretic semantics for SemNet
- Mathematical Knowledge Management
- A compact kernel for the calculus of inductive constructions
- Proof assistants: history, ideas and future
- scientific article; zbMATH DE number 1420794 (Why is no real title available?)
- Unifiers as equivalences: proof-relevant unification of dependently typed data
- Proof by computation in the Coq system
- Faking it Simulating dependent types in Haskell
- jsCoq
- Advanced Functional Programming
- scientific article; zbMATH DE number 1927413 (Why is no real title available?)
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- An overview of the Tecton proof system
- scientific article; zbMATH DE number 1701346 (Why is no real title available?)
- Type theory should eat itself
- Types for Proofs and Programs
- Proof-search in type-theoretic languages: An introduction
- Constructive membership predicates as index types
- Using typed lambda calculus to implement formal systems on a machine
- scientific article; zbMATH DE number 1301731 (Why is no real title available?)
- More Church-Rosser proofs (in Isabelle/HOL)
- Ynot: dependent types for imperative programs
- Normalization for the simply-typed lambda-calculus in Twelf
- A focused sequent calculus framework for proof search in pure type systems
- scientific article; zbMATH DE number 891219 (Why is no real title available?)
- A higher-order calculus and theory abstraction
- Unifying Sets and Programs via Dependent Types
- scientific article; zbMATH DE number 1863382 (Why is no real title available?)
- The practice of logical frameworks
- scientific article; zbMATH DE number 1420791 (Why is no real title available?)
- The seventeen provers of the world. Foreword by Dana S. Scott..
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- A Dependently Typed Framework for Static Analysis of Program Execution Costs
- A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits
- scientific article; zbMATH DE number 1301735 (Why is no real title available?)
- scientific article; zbMATH DE number 1231611 (Why is no real title available?)
- Program specification and data refinement in type theory
- Alpha equivalence equalities
- Two case studies of semantics execution in Maude: CCS and LOTOS
- ProofWidgets
- scientific article; zbMATH DE number 1863396 (Why is no real title available?)
- Unifying sets and programs via dependent types
- On the role of OpenMath in interactive mathematical documents
- Dependently typed records in type theory
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- Categorical abstract machines for higher-order typed -calculi
- A Normalizing Intuitionistic Set Theory with Inaccessible Sets
- scientific article; zbMATH DE number 1231700 (Why is no real title available?)
- Functional and Logic Programming
- Equations: a dependent pattern-matching compiler
- Manifest Fields and Module Mechanisms in Intensional Type Theory
- scientific article; zbMATH DE number 1670760 (Why is no real title available?)
- Kinded type inference for parametric overloading
- The seven virtues of simple type theory
- Machine Translation and Type Theory
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- Exploring abstract algebra in constructive type theory
- Internal type theory
- scientific article; zbMATH DE number 1005001 (Why is no real title available?)
- Termination checking with types
- scientific article; zbMATH DE number 591911 (Why is no real title available?)
- Coercion completion and conservativity in coercive subtyping
- Generation and presentation of formal mathematical documents
- Dealing with algebraic expressions over a field in Coq using Maple
- A language-based approach to functionally correct imperative programming
- Simply-typed underdeterminism
- An experiment concerning mathematical proofs on computers with French undergraduate students
- scientific article; zbMATH DE number 1420782 (Why is no real title available?)
- scientific article; zbMATH DE number 2185673 (Why is no real title available?)
- Ivor, a Proof Engine
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- An induction principle for pure type systems
- Types for Proofs and Programs
- Indexed types
- scientific article; zbMATH DE number 1512607 (Why is no real title available?)
- scientific article; zbMATH DE number 2085175 (Why is no real title available?)
- A natural deduction approach to dynamic logic
- The extended calculus of constructions (ECC) with inductive types
- The locally nameless representation
- scientific article; zbMATH DE number 1765684 (Why is no real title available?)
- A two-level approach towards lean proof-checking
- On -conversion in the -cube and the combination with abbreviations
- scientific article; zbMATH DE number 2080759 (Why is no real title available?)
- Some lambda calculus and type theory formalized
- Inductive families
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A canonical locally named representation of binding
- Proof planning for strategy development
- Comparing higher-order encodings in logical frameworks and tile logic
- Transitivity in coercive subtyping
- Coq
This page was built for software: LEGO
