ALF

swMATH8603MaRDI QIDQ20609

No author found.

Related Items (67)

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

This page was built for software: ALF