scientific article
From MaRDI portal
Publication:3703866
zbMath0581.03007MaRDI QIDQ3703866
Publication date: 1985
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Combinatory logic and lambda calculus (03B40)
Related Items
Inductively defined types in the Calculus of Constructions ⋮ Formalizing generalized maps in Coq ⋮ Formalizing the trading theorem in Coq ⋮ An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps ⋮ A higher-order calculus and theory abstraction ⋮ History and basic features of the critical-pair/completion procedure ⋮ Design and formal proof of a new optimal image segmentation program with hypermaps ⋮ An effective proof of the well-foundedness of the multiset path ordering ⋮ The calculus of constructions ⋮ A small complete category ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ On modular properties of higher order extensional lambda calculi ⋮ Generalization from partial parametrization in higher-order type theory ⋮ Characteristics of de Bruijn’s early proof checker Automath ⋮ A complete proof system for propositional projection temporal logic ⋮ Formal specification and proofs for the topology and classification of combinatorial surfaces ⋮ Proving strong normalization of CC by modifying realizability semantics ⋮ Conservativity between logics and typed λ calculi ⋮ Programming with streams in Coq a case study: The Sieve of Eratosthenes ⋮ Do-it-yourself type theory ⋮ Constructive system for automatic program synthesis ⋮ A characterization of lambda definable tree operations ⋮ A modest model of records, inheritance, and bounded quantification ⋮ Between constructive mathematics and PROLOG ⋮ Type checking with universes ⋮ Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof ⋮ Categorical ML -- category-theoretic modular programming ⋮ Constructing type systems over an operational semantics ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Definition and basic properties of the Deva meta-calculus ⋮ Inductive-data-type systems ⋮ On the proof theory of Coquand's calculus of constructions ⋮ A formal proof of the deadline driven scheduler in PPTL axiomatic system ⋮ Functorial polymorphism ⋮ Syntax for Free: Representing Syntax with Binding Using Parametricity ⋮ Structures definable in polymorphism ⋮ From term models to domains ⋮ The foundation of a generic theorem prover ⋮ Computational foundations of basic recursive function theory ⋮ Synthesis of ML programs in the system Coq ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
Uses Software
