The following pages link to ALF (Q20609):
Displayed 50 items.
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- The proof monad (Q974136) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Type inference for pure type systems (Q1271309) (← links)
- A note on complexity measures for inductive classes in constructive type theory (Q1271558) (← links)
- A constructive theory of ordered affine geometry (Q1279729) (← links)
- A constructive approach to state description semantics (Q1414570) (← links)
- The calculus of constructions as a framework for proof search with set variable instantiation (Q1575927) (← links)
- Comparing and implementing calculi of explicit substitutions with eta-reduction (Q1779307) (← links)
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions (Q1850959) (← links)
- Higher-order substitutions (Q1854398) (← links)
- On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions (Q1854404) (← links)
- The axioms of constructive geometry (Q1902978) (← links)
- Formalizing constructive projective geometry in Agda (Q2333313) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- Dependent types and explicit substitutions: a meta-theoretical development (Q2713354) (← links)
- (Q2766802) (← links)
- Incompleteness, Undecidability and Automated Proofs (Q2829997) (← links)
- PVS#: Streamlined Tacticals for PVS (Q2864359) (← links)
- Imperative LF Meta-Programming (Q2871844) (← links)
- (Q3024857) (← links)
- (Q3024905) (← links)
- Records and Record Types in Semantic Theory (Q3025327) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- Crafting a Proof Assistant (Q3612433) (← links)
- Algebra of programming in Agda: Dependent types for relational program derivation (Q3644935) (← links)
- A coherence theorem for Martin-Löf's type theory (Q4236885) (← links)
- (Q4246943) (← links)
- (Q4249901) (← links)
- (Q4263084) (← links)
- (Q4281462) (← links)
- (Q4281483) (← links)
- (Q4411846) (← links)
- (Q4484338) (← links)
- Relating the - and s-styles of explicit substitutions (Q4500175) (← links)
- Type checking dependent (record) types and subtyping (Q4500363) (← links)
- (Q4524768) (← links)
- (Q4525278) (← links)
- Type theoretic semantics for SemNet (Q4632324) (← links)
- A two-level approach towards lean proof-checking (Q4647567) (← links)
- A constructive proof of the Heine-Borel covering theorem for formal reals (Q4647570) (← links)
- An application of co-inductive types in Coq: Verification of the alternating bit protocol (Q4647576) (← links)
- An algorithm for checking incomplete proof objects in type theory with localization and unification (Q4647580) (← links)
- Context-relative syntactic categories and the formalization of mathematical text (Q4647583) (← links)
- Optimized encodings of fragments of type theory in first order logic (Q4647585) (← links)
- (Q4736398) (← links)
- (Q4790656) (← links)
- (Q4823135) (← links)
- (Q4880706) (← links)