swMATH8603MaRDI QIDQ20609FDOQ20609
Author name not available (Why is that?)
Official website: https://homepages.inf.ed.ac.uk/wadler/realworld/alf.html
Cited In (81)
- Title not available (Why is that?)
- Machine Translation and Type Theory
- Title not available (Why is that?)
- A two-level approach towards lean proof-checking
- Context-relative syntactic categories and the formalization of mathematical text
- Type checking dependent (record) types and subtyping
- 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
- Contextual modal type theory
- Representing model theory in a type-theoretical logical framework
- 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?)
- Optimized encodings of fragments of type theory in first order logic
- Types for Proofs and Programs
- Primitive recursion for higher-order abstract syntax
- Type inference for pure type systems
- Indexed induction-recursion
- 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?)
- Nuprl
- Automath
- Plastic
- Artificial Intelligence and Symbolic Computation
- GF
- Polyp
- gaia
- Cayenne
- LEGO
- MicroRogue
- GF
- Inductive beluga: programming proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- A coherence theorem for Martin-Löf's type theory
- Elf
- PAL+
- FreshOCaml
- FraCaS
- 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
- Translating between language and logic: what is easy and what is difficult
- Comparing and implementing calculi of explicit substitutions with eta-reduction
- Comparing calculi of explicit substitutions with eta-reduction
- Crafting a Proof Assistant
- A constructive approach to state description semantics
- An application of co-inductive types in Coq: verification of the alternating bit protocol
- 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
- 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?)
- Tactics and parameters
- 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
