LEGO

swMATH9685MaRDI QIDQ21664FDOQ21664

Author name not available (Why is that?)

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

Cited In (only showing first 100 items - show all)

• The seventeen provers of the world. Foreword by Dana S. Scott..
• A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits
• Title not available (Why is that?)
• Title not available (Why is that?)
• Program specification and data refinement in type theory
• On the role of OpenMath in interactive mathematical documents
• Two case studies of semantics execution in Maude: CCS and LOTOS
• Alpha equivalence equalities
• Unifying sets and programs via dependent types
• A Normalizing Intuitionistic Set Theory with Inaccessible Sets
• Dependently typed records in type theory
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• Equations: a dependent pattern-matching compiler
• Functional and Logic Programming
• Categorical abstract machines for higher-order typed \(\lambda\)-calculi
• Title not available (Why is that?)
• Exploring abstract algebra in constructive type theory
• Internal type theory
• The seven virtues of simple type theory
• Title not available (Why is that?)
• Termination checking with types
• Title not available (Why is that?)
• Coercion completion and conservativity in coercive subtyping
• A language-based approach to functionally correct imperative programming
• Title not available (Why is that?)
• Simply-typed underdeterminism
• Ivor, a Proof Engine
• Title not available (Why is that?)
• Title not available (Why is that?)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Indexed types
• A natural deduction approach to dynamic logic
• The extended calculus of constructions (ECC) with inductive types
• The locally nameless representation
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• Some lambda calculus and type theory formalized
• Inductive families
• A canonical locally named representation of binding
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Proof planning for strategy development
• Title not available (Why is that?)
• Title not available (Why is that?)
• \(\pi\)-calculus in (Co)inductive-type theory
• Verifying programs in the calculus of inductive constructions
• HYBRID
• Order-sorted inductive types
• Title not available (Why is that?)
• ML
• Search algorithms in type theory
• Special issue: Formal proof
• Type-level computation using narrowing in \(\Omega\)mega
• Artificial Intelligence and Symbolic Computation
• Cayenne
• Epigram
• Minlog
• PoplMark
• SAFL
• XBarnacle
• TIL
• Cambridge LCF
• Autarkic computations in formal proofs
• Theorem Proving in Higher Order Logics
• Metacircularity in the polymorphic \(\lambda\)-calculus
• Type checking with universes
• Mathematical Knowledge Management
• A compact kernel for the calculus of inductive constructions
• Proof assistants: history, ideas and future
• Proof by computation in the Coq system
• Title not available (Why is that?)
• Title not available (Why is that?)
• An overview of the Tecton proof system
• Title not available (Why is that?)
• Ynot: dependent types for imperative programs
• Using typed lambda calculus to implement formal systems on a machine
• Title not available (Why is that?)
• A higher-order calculus and theory abstraction
• The practice of logical frameworks
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Dependently Typed Framework for Static Analysis of Program Execution Costs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Machine Translation and Type Theory
• Kinded type inference for parametric overloading
• Martin Hofmann’s contributions to type theory: Groupoids and univalence
• Generation and presentation of formal mathematical documents
• Dealing with algebraic expressions over a field in Coq using Maple
• An experiment concerning mathematical proofs on computers with French undergraduate students
• Title not available (Why is that?)
• An induction principle for pure type systems
• Types for Proofs and Programs
• A two-level approach towards lean proof-checking
• Title not available (Why is that?)
• Title not available (Why is that?)
• Comparing higher-order encodings in logical frameworks and tile logic
• Transitivity in coercive subtyping
• Structural subtyping for inductive types with functorial equality rules
• A partial type checking algorithm for Type:Type

This page was built for software: LEGO