ALF
From MaRDI portal
Cited in
(82)- Proof assistants: history, ideas and future
- Type inference for pure type systems
- A note on complexity measures for inductive classes in constructive type theory
- A constructive theory of ordered affine geometry
- A constructive approach to state description semantics
- TinkerType
- The calculus of constructions as a framework for proof search with set variable instantiation
- Comparing and implementing calculi of explicit substitutions with eta-reduction
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Higher-order substitutions
- On the formalization of the modal -calculus in the calculus of inductive constructions
- Nuprl
- The axioms of constructive geometry
- Automath
- Plastic
- GF
- Polyp
- gaia
- LEGO
- Cayenne
- Formalizing constructive projective geometry in Agda
- MicroRogue
- GF
- Indexed induction-recursion
- Dependent types and explicit substitutions: A meta-theoretical development
- scientific article; zbMATH DE number 1696611 (Why is no real title available?)
- Incompleteness, Undecidability and Automated Proofs
- PVS\#: streamlined tacticals for PVS
- Imperative LF meta-programming
- scientific article; zbMATH DE number 2185680 (Why is no real title available?)
- scientific article; zbMATH DE number 2185713 (Why is no real title available?)
- Records and Record Types in Semantic Theory
- Elf
- PAL+
- FreshOCaml
- Inductive beluga: programming proofs
- Crafting a Proof Assistant
- Algebra of programming in Agda: Dependent types for relational program derivation
- FraCaS
- A coherence theorem for Martin-Löf's type theory
- scientific article; zbMATH DE number 1301730 (Why is no real title available?)
- scientific article; zbMATH DE number 1303348 (Why is no real title available?)
- scientific article; zbMATH DE number 1341542 (Why is no real title available?)
- scientific article; zbMATH DE number 512769 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 1948185 (Why is no real title available?)
- scientific article; zbMATH DE number 1927420 (Why is no real title available?)
- Relating the - and s-styles of explicit substitutions
- Type checking dependent (record) types and subtyping
- scientific article; zbMATH DE number 1552510 (Why is no real title available?)
- scientific article; zbMATH DE number 1555179 (Why is no real title available?)
- Type theoretic semantics for SemNet
- 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
- scientific article; zbMATH DE number 2085174 (Why is no real title available?)
- scientific article; zbMATH DE number 1863381 (Why is no real title available?)
- scientific article; zbMATH DE number 2110615 (Why is no real title available?)
- scientific article; zbMATH DE number 891219 (Why is no real title available?)
- Comparing calculi of explicit substitutions with eta-reduction
- Tactics and parameters
- scientific article; zbMATH DE number 1420785 (Why is no real title available?)
- Translating between language and logic: what is easy and what is difficult
- Machine Translation and Type Theory
- Contextual modal type theory
- Mathematical Knowledge Management
- Artificial Intelligence and Symbolic Computation
- Types for Proofs and Programs
- Types for Proofs and Programs
- scientific article; zbMATH DE number 2238212 (Why is no real title available?)
- Types for Proofs and Programs
- Types for Proofs and Programs
- 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
- Representing model theory in a type-theoretical logical framework
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- The proof monad
This page was built for software: ALF
