A type-theoretical alternative to ISWIM, CUCH, OWHY

DOI10.1016/0304-3975(93)90095-BzbMath0942.68522OpenAlexW2010959827WikidataQ29037708 ScholiaQ29037708MaRDI QIDQ1314363

Publication date: 26 February 1996

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(93)90095-b

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40) Abstract and axiomatic computability and recursion theory (03D75)

Related Items

The origins of structural operational semantics, An approach to deciding the observational equivalence of Algol-like languages, On the $\lambda Y$ calculus, The Scott model of PCF in univalent type theory, Formalizing non-termination of recursive programs, HOL Light: An Overview, Towards the computational complexity of $\mathcal{PR}^ \omega$-terms, Two categories of effective continuous cpos, A two-valued logic for properties of strict functional programs allowing partial functions, Full abstraction and the Context Lemma (preliminary report), A general adequacy result for a linear functional language, Categorical semantics of a simple differential programming language, Formalising Mathematics in Simple Type Theory, Weakly weighted generalised quasi-metric spaces and semilattices, Apartness, sharp elements, and the Scott topology of domains, No value restriction is needed for algebraic effects and handlers, Hierarchies of total functionals over the reals, Reference counting as a computational interpretation of linear logic, Densities of almost surely terminating probabilistic programs are differentiable almost everywhere, Fixpoints and Search in PVS, A monad for randomized algorithms, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, Continuous Domain Theory in Logical Form, Partiality and recursion in interactive theorem provers – an overview, A stable programming language, On the ubiquity of certain total type structures, Relationships between classes of monotonic functions, Functionals computable in series and in parallel, Executable Relational Specifications of Polymorphic Type Systems Using Prolog, From Logic to Theoretical Computer Science – An Update, On Natural Non-dcpo Domains, Semi-decidability of May, Must and Probabilistic Testing in a Higher-type Setting, N. G. de Bruijn's contribution to the formalization of mathematics, Unnamed Item, Operational domain theory and topology of sequential programming languages, Can LCF be topped! Flat lattice models of typed $\lambda{}$-calculus, On the completeness of order-theoretic models of the $\lambda $-calculus, Automata, Logic and Games for the $$\lambda $$ -Calculus, A topology on lattice-ordered groups, Natural non-dcpo domains and f-spaces, Computing with Functionals—Computability Theory or Computer Science?, Induction and recursion on the partial real line with applications to Real PCF, The extensional ordering of the sequential functionals, Domain semantics of possibility computations, Dynamic game semantics, A game-semantic model of computation, The sequential functionals of type $(\iota \rightarrow \iota)^n \rightarrow \iota$ form a dcpo for all $n \in \Bbb N$, Decidability of behavioural equivalence in unary PCF, Proof assistants: history, ideas and future, Properly injective spaces and function spaces, Sequential algorithms and strongly stable functions, The sequentially realizable functionals, Definability and Full Abstraction, Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL, Computational foundations of basic recursive function theory, Partially ordered objects in a topos, Relative definability of boolean functions via hypergraphs, Exact real number computations relative to hereditarily total functionals., PLANS AND PLANNING IN MATHEMATICAL PROOFS

Cites Work