Beluga

From MaRDI portal
Software:14061



swMATH1321MaRDI QIDQ14061


No author found.





Related Items (27)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A surveyFunctions-as-constructors higher-order unification: extended pattern unificationInductive Beluga: Programming ProofsThere Is No Best $$\beta $$ -Normalization Strategy for Higher-Order ReasonersProof-relevant Horn Clauses for Dependent Type Inference and Term SynthesisProgramming Type-Safe Transformations Using Higher-Order Abstract SyntaxMechanizing type environments in weak HOASPOPLMark reloaded: Mechanizing proofs by logical relationsA Modular Type Reconstruction AlgorithmExtensible Datasort RefinementsLINCX: A Linear Logical Framework with First-Class ContextsHigher-Order Dynamic Pattern Unification for Dependent Types and RecordsProof Pearl: Abella Formalization of λ-Calculus Cube Property$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monadsBinders unboundReasoning with Higher-Order Abstract Syntax and Contexts: A ComparisonProgramming Inductive Proofs\(\mathrm{HO}\pi\) in CoqA Higher-Order Abstract Syntax Approach to Verified Transformations on Functional ProgramsUnnamed ItemHarpoon: mechanizing metatheory interactivelyA case study in programming coinductive proofs: Howe’s methodMechanized metatheory revisitedFunctions-as-constructors Higher-order UnificationFormalization of metatheory of the Quipper quantum programming language in a linear logicRensets and renaming-based recursion for syntax with bindings\texttt{slepice}: towards a verified implementation of type theory in type theory


This page was built for software: Beluga