ALF

swMATH8603MaRDI QIDQ20609FDOQ20609

Author name not available (Why is that?)

Cited In (67)

• A two-level approach towards lean proof-checking
• Context-relative syntactic categories and the formalization of mathematical text
• Types for Proofs and Programs
• Proof-term synthesis on dependent-type systems via explicit substitutions
• Types for Proofs and Programs
• Relating the   - and  s-styles of explicit substitutions
• Title not available (Why is that?)
• Contextual modal type theory
• Representing model theory in a type-theoretical logical framework
• Machine Translation and Type Theory
• A note on complexity measures for inductive classes in constructive type theory
• The proof monad
• Title not available (Why is that?)
• Title not available (Why is that?)
• An implementation of LF with coercive subtyping and universes
• A constructive theory of ordered affine geometry
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• Title not available (Why is that?)
• Title not available (Why is that?)
• Optimized encodings of fragments of type theory in first order logic
• Types for Proofs and Programs
• Comparing Calculi of Explicit Substitutions with Eta-reduction
• An application of co-inductive types in Coq: Verification of the alternating bit protocol
• Primitive recursion for higher-order abstract syntax
• Type checking dependent (record) types and subtyping
• Type inference for pure type systems
• Indexed induction-recursion
• Translating between Language and Logic: What Is Easy and What Is Difficult
• The axioms of constructive geometry
• Higher-order substitutions
• A constructive proof of the Heine-Borel covering theorem for formal reals
• Title not available (Why is that?)
• Title not available (Why is that?)
• Types for Proofs and Programs
• Title not available (Why is that?)
• Artificial Intelligence and Symbolic Computation
• Tactics and Parameters
• Title not available (Why is that?)
• Title not available (Why is that?)
• A coherence theorem for Martin-Löf's type theory
• On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
• Type theoretic semantics for SemNet
• Mathematical Knowledge Management
• PVS\#: streamlined tacticals for PVS
• Incompleteness, Undecidability and Automated Proofs
• Proof assistants: history, ideas and future
• Title not available (Why is that?)
• Formalizing constructive projective geometry in Agda
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Crafting a Proof Assistant
• A constructive approach to state description semantics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Records and Record Types in Semantic Theory
• The calculus of constructions as a framework for proof search with set variable instantiation
• Algebra of programming in Agda: Dependent types for relational program derivation
• Inductive Beluga: Programming Proofs
• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
• Dependent types and explicit substitutions: A meta-theoretical development
• An algorithm for checking incomplete proof objects in type theory with localization and unification
• Title not available (Why is that?)
• Imperative LF meta-programming
• Title not available (Why is that?)
• Studies of a theory of specifications with built-in program extraction
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for software: ALF