LEGO

MaRDI QIDQ21664swMATHFDO

Official website http://www.dcs.ed.ac.uk/home/lego/

Cited in

(only showing first 100 items - show all)

• Proof assistants: history, ideas and future
• A compact kernel for the calculus of inductive constructions
• Type checking with universes
• Metacircularity in the polymorphic \(\lambda\)-calculus
• The extended calculus of constructions (ECC) with inductive types
• Verifying programs in the calculus of inductive constructions
• Simply-typed underdeterminism
• Order-sorted inductive types
• Coq
• On -conversion in the -cube and the combination with abbreviations
• HYBRID
• Inductive families
• An overview of the Tecton proof system
• Categorical abstract machines for higher-order typed -calculi
• jsCoq
• Indexed types
• ML
• Search algorithms in type theory
• Proof-search in type-theoretic languages: An introduction
• -calculus in (Co)inductive-type theory
• Proof planning for strategy development
• Autarkic computations in formal proofs
• Transitivity in coercive subtyping
• Nuprl
• An experiment concerning mathematical proofs on computers with French undergraduate students
• Kinded type inference for parametric overloading
• Automath
• Plastic
• The locally nameless representation
• Special issue: Formal proof
• Some lambda calculus and type theory formalized
• ALF
• Cayenne
• Epigram
• Minlog
• CtCoq
• PoplMark
• Analytica
• AURA
• A canonical locally named representation of binding
• Dealing with algebraic expressions over a field in Coq using Maple
• SAFL
• A higher-order calculus and theory abstraction
• LOTOSphere
• scientific article; zbMATH DE number 1615229 (Why is no real title available?)
• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 1670760 (Why is no real title available?)
• Generation and presentation of formal mathematical documents
• scientific article; zbMATH DE number 1701346 (Why is no real title available?)
• Type theory should eat itself
• Comparing higher-order encodings in logical frameworks and tile logic
• Constructive membership predicates as index types
• Type-level computation using narrowing in \(\Omega\)mega
• Normalization for the simply-typed lambda-calculus in Twelf
• A language-based approach to functionally correct imperative programming
• Unifiers as equivalences: proof-relevant unification of dependently typed data
• A focused sequent calculus framework for proof search in pure type systems
• scientific article; zbMATH DE number 2185673 (Why is no real title available?)
• XBarnacle
• Faking it Simulating dependent types in Haskell
• Elf
• TIL
• mini-ML
• Structural subtyping for inductive types with functorial equality rules
• Unifying Sets and Programs via Dependent Types
• Ivor, a Proof Engine
• A Dependently Typed Framework for Static Analysis of Program Execution Costs
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• SKIL
• Gallina
• Tecton
• AFFIRM
• Unifying sets and programs via dependent types
• scientific article; zbMATH DE number 1231611 (Why is no real title available?)
• scientific article; zbMATH DE number 1231700 (Why is no real title available?)
• scientific article; zbMATH DE number 1301731 (Why is no real title available?)
• scientific article; zbMATH DE number 1301735 (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?)
• Program specification and data refinement in type theory
• Alpha equivalence equalities
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 1005001 (Why is no real title available?)
• Cambridge LCF
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• scientific article; zbMATH DE number 2080759 (Why is no real title available?)
• scientific article; zbMATH DE number 1927413 (Why is no real title available?)
• scientific article; zbMATH DE number 1512607 (Why is no real title available?)
• scientific article; zbMATH DE number 1765684 (Why is no real title available?)
• Type theoretic semantics for SemNet
• A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits
• More Church-Rosser proofs (in Isabelle/HOL)
• A two-level approach towards lean proof-checking
• Internal type theory
• A natural deduction approach to dynamic logic
• Termination checking with types
• scientific article; zbMATH DE number 2085175 (Why is no real title available?)
• scientific article; zbMATH DE number 1863382 (Why is no real title available?)
• scientific article; zbMATH DE number 1863396 (Why is no real title available?)
• scientific article; zbMATH DE number 2090315 (Why is no real title available?)

This page was built for software: LEGO