LEGO

swMATH9685MaRDI QIDQ21664

No author found.

Related Items (only showing first 100 items - show all)

Ynot ⋮ The seventeen provers of the world. Foreword by Dana S. Scott.. ⋮ Inductive families ⋮ An experiment concerning mathematical proofs on computers with French undergraduate students ⋮ An overview of the Tecton proof system ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Categorical abstract machines for higher-order typed \(\lambda\)-calculi ⋮ A higher-order calculus and theory abstraction ⋮ Unnamed Item ⋮ Program specification and data refinement in type theory ⋮ More Church-Rosser proofs (in Isabelle/HOL) ⋮ Unnamed Item ⋮ A canonical locally named representation of binding ⋮ Kinded type inference for parametric overloading ⋮ Unnamed Item ⋮ Martin Hofmann’s contributions to type theory: Groupoids and univalence ⋮ A language-based approach to functionally correct imperative programming ⋮ Types for Proofs and Programs ⋮ Unnamed Item ⋮ Advanced Functional Programming ⋮ Unnamed Item ⋮ Indexed types ⋮ Unnamed Item ⋮ Unifying sets and programs via dependent types ⋮ Unnamed Item ⋮ The locally nameless representation ⋮ Unnamed Item ⋮ Alpha equivalence equalities ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Unnamed Item ⋮ Special issue: Formal proof ⋮ Some lambda calculus and type theory formalized ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ Unifiers as equivalences: proof-relevant unification of dependently typed data ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Type checking with universes ⋮ Metacircularity in the polymorphic \(\lambda\)-calculus ⋮ Type theoretic semantics for SemNet ⋮ Dealing with algebraic expressions over a field in Coq using Maple ⋮ Unnamed Item ⋮ A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems ⋮ The seven virtues of simple type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits ⋮ The extended calculus of constructions (ECC) with inductive types ⋮ A two-level approach towards lean proof-checking ⋮ Internal type theory ⋮ A natural deduction approach to dynamic logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ A Partial Type Checking Algorithm for Type:Type ⋮ Termination checking with types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Dependently typed records in type theory ⋮ A Normalizing Intuitionistic Set Theory with Inaccessible Sets ⋮ Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. ⋮ Equations: A Dependent Pattern-Matching Compiler ⋮ Transitivity in coercive subtyping ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unifying Sets and Programs via Dependent Types ⋮ Ivor, a Proof Engine ⋮ Unnamed Item ⋮ Type Theory Should Eat Itself ⋮ Artificial Intelligence and Symbolic Computation ⋮ Exploring abstract algebra in constructive type theory ⋮ A Dependently Typed Framework for Static Analysis of Program Execution Costs ⋮ Verifying programs in the calculus of inductive constructions ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ Theorem Proving in Higher Order Logics ⋮ Simply-typed underdeterminism ⋮ Unnamed Item ⋮ Functional and Logic Programming ⋮ Unnamed Item ⋮ Order-sorted inductive types ⋮ Unnamed Item ⋮ Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic ⋮ Proof assistants: history, ideas and future ⋮ A compact kernel for the calculus of inductive constructions ⋮ Search algorithms in type theory ⋮ Proof-search in type-theoretic languages: An introduction ⋮ On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations ⋮ Machine Translation and Type Theory ⋮ \(\pi\)-calculus in (Co)inductive-type theory ⋮ Mathematical Knowledge Management ⋮ Constructive Membership Predicates as Index Types ⋮ Type-level Computation Using Narrowing in Ωmega ⋮ Proof planning for strategy development ⋮ Normalization for the Simply-Typed Lambda-Calculus in Twelf ⋮ Faking it Simulating dependent types in Haskell ⋮ Autarkic computations in formal proofs ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS

This page was built for software: LEGO