ALF
From MaRDI portal
Cited in
(82)- Studies of a theory of specifications with built-in program extraction
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 1927420 (Why is no real title available?)
- Types for Proofs and Programs
- Relating the - and s-styles of explicit substitutions
- Representing model theory in a type-theoretical logical framework
- scientific article; zbMATH DE number 1420785 (Why is no real title available?)
- Contextual modal type theory
- Machine Translation and Type Theory
- A note on complexity measures for inductive classes in constructive type theory
- The proof monad
- scientific article; zbMATH DE number 2185680 (Why is no real title available?)
- scientific article; zbMATH DE number 1303348 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 2238212 (Why is no real title available?)
- scientific article; zbMATH DE number 1341542 (Why is no real title available?)
- Optimized encodings of fragments of type theory in first order logic
- Types for Proofs and Programs
- A two-level approach towards lean proof-checking
- Context-relative syntactic categories and the formalization of mathematical text
- Type inference for pure type systems
- Primitive recursion for higher-order abstract syntax
- Type checking dependent (record) types and subtyping
- Indexed induction-recursion
- The axioms of constructive geometry
- Higher-order substitutions
- TinkerType
- Nuprl
- Automath
- Plastic
- GF
- Polyp
- gaia
- Cayenne
- LEGO
- MicroRogue
- GF
- Elf
- PAL+
- FreshOCaml
- FraCaS
- scientific article; zbMATH DE number 512769 (Why is no real title available?)
- A constructive proof of the Heine-Borel covering theorem for formal reals
- scientific article; zbMATH DE number 2185713 (Why is no real title available?)
- scientific article; zbMATH DE number 1301730 (Why is no real title available?)
- Types for Proofs and Programs
- Artificial Intelligence and Symbolic Computation
- Inductive beluga: programming proofs
- scientific article; zbMATH DE number 1555179 (Why is no real title available?)
- scientific article; zbMATH DE number 1863381 (Why is no real title available?)
- On the formalization of the modal -calculus in the calculus of inductive constructions
- A coherence theorem for Martin-Löf's type theory
- Types for Proofs and Programs
- Type theoretic semantics for SemNet
- Mathematical Knowledge Management
- PVS\#: streamlined tacticals for PVS
- Proof assistants: history, ideas and future
- Incompleteness, Undecidability and Automated Proofs
- scientific article; zbMATH DE number 1696611 (Why is no real title available?)
- Formalizing constructive projective geometry in Agda
- Comparing and implementing calculi of explicit substitutions with eta-reduction
- Translating between language and logic: what is easy and what is difficult
- Comparing calculi of explicit substitutions with eta-reduction
- A constructive approach to state description semantics
- Crafting a Proof Assistant
- An application of co-inductive types in Coq: verification of the alternating bit protocol
- scientific article; zbMATH DE number 2110615 (Why is no real title available?)
- Records and Record Types in Semantic Theory
- scientific article; zbMATH DE number 2085174 (Why is no real title available?)
- scientific article; zbMATH DE number 1948185 (Why is no real title available?)
- 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
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Proof-term synthesis on dependent-type systems via explicit substitutions
- Dependent types and explicit substitutions: A meta-theoretical development
- Imperative LF meta-programming
- An algorithm for checking incomplete proof objects in type theory with localization and unification
- scientific article; zbMATH DE number 891219 (Why is no real title available?)
- Tactics and parameters
- scientific article; zbMATH DE number 1552510 (Why is no real title available?)
This page was built for software: ALF
