scientific article
From MaRDI portal
Publication:2778806
zbMath0995.68018MaRDI QIDQ2778806
Publication date: 21 March 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Theory of programming languages (68N15)
Related Items
Session-based concurrency, declaratively ⋮ Data-driven adaptation for smart sessions ⋮ Gradual typing using union typing with records ⋮ Parametric parameter passing \(\lambda\)-calculus ⋮ Efficient virtual machine support of runtime structural reflection ⋮ Dependently typed array programs don't go wrong ⋮ Nonlinear pattern matching in rule-based modeling languages ⋮ Self-adaptation and secure information flow in multiparty communications ⋮ A program logic for fresh name generation ⋮ Directly reflective meta-programming ⋮ Abstraction and subsumption in modular verification of C programs ⋮ Polymorphic typed defunctionalization and concretization ⋮ Creol: A type-safe object-oriented model for distributed concurrent systems ⋮ Multiparty session types, beyond duality ⋮ Composition-nominative logics as institutions ⋮ Type checking a multithreaded functional language with session types ⋮ Functional sets with typed symbols: Mixed zonotopes and polynotopes for hybrid nonlinear reachability and filtering ⋮ Modeling grammatical evolution by automaton ⋮ Well-definedness and semantic type-checking for the nested relational calculus ⋮ On the value of variables ⋮ Model approach to grammatical evolution: theory and case study ⋮ Tyrolean termination tool: techniques and features ⋮ Adding recursion to Dpi ⋮ Comparing type systems for deadlock freedom ⋮ Simple and safe SQL queries with \texttt{C++} templates ⋮ A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Intuitionistic completeness of first-order logic ⋮ The rewriting logic semantics project: a progress report ⋮ A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation ⋮ Conversation types ⋮ A graph-based generic type system for object-oriented programs ⋮ Unifying sets and programs via dependent types ⋮ Justification logic as a foundation for certifying mobile computation ⋮ Precise subtyping for synchronous multiparty sessions ⋮ A reduction semantics for direct-style asynchronous observables ⋮ Mechanizing type environments in weak HOAS ⋮ Typed path polymorphism ⋮ Variability encoding: from compile-time to load-time variability ⋮ An algebra of behavioural types ⋮ Typed context awareness ambient calculus for pervasive applications ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ ASP\(_{\text{fun}}\) : a typed functional active object calculus ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ A relational realizability model for higher-order stateful ADTs ⋮ Membership(s) and compliance(s) with class-based graphs ⋮ Region analysis for deductive verification of C programs ⋮ Typing access control and secure information flow in sessions ⋮ Type-based termination of generic programs ⋮ Parametric \(\lambda \)-theories ⋮ Integrating deployment architectures and resource consumption in timed object-oriented models ⋮ Verified software units ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ Towards proving type safety of .NET CIL ⋮ Formalising Java RMI with explicit code mobility ⋮ Domain-theoretical models of parametric polymorphism ⋮ Type soundness for path polymorphism ⋮ Translating higher-order clauses to first-order clauses ⋮ Towards proving type safety of \(\mathrm{C}^{\#}\) ⋮ Flag-based big-step semantics ⋮ Monitoring networks through multiparty session types ⋮ The spirit of ghost code ⋮ Composition and decomposition of multiparty sessions ⋮ Structural types for systems of equations: type refinements for structurally dynamic first-class modular systems of equations ⋮ A type system for counting instances of software components ⋮ A type system for reflective program generators ⋮ A language for generic programming in the large ⋮ On quantified linear implications ⋮ Delegation by object composition ⋮ Amalgamation in the semantics of CASL ⋮ Verifying pointer and string analyses with region type systems ⋮ On the complexity of deciding typability in the relational algebra ⋮ Fundamentals of session types ⋮ Type inference and strong static type checking for Promela ⋮ Global types with internal delegation ⋮ Two algorithms in search of a type-system ⋮ Amalgamating sessions and methods in object-oriented languages with generics ⋮ The stream-based service-centred calculus: a foundation for service-oriented programming ⋮ Partial and complete processes in multiparty sessions ⋮ HasCasl: integrated higher-order specification and program development ⋮ Implementing type systems for the IDE with Xsemantics ⋮ A descriptive type foundation for RDF Schema ⋮ A rewriting logic approach to operational semantics ⋮ Featherweight Java with dynamic and static overloading ⋮ Objects and session types ⋮ Recasting ML\(^{\text F}\) ⋮ Enhanced type inference for binding-time analysis ⋮ A correspondence between type checking via reduction and type checking via evaluation ⋮ A trace-based model for multiparty contracts ⋮ Refined typing to localize the impact of forced strictness on free theorems ⋮ Reversible sessions with flexible choices ⋮ QPCF: higher-order languages and quantum circuits ⋮ Semantic essence of AsmL ⋮ Observational program calculi and the correctness of translations ⋮ MOMI: a calculus for mobile mixins ⋮ Subtyping for session types in the pi calculus ⋮ Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus ⋮ From specification to testing: semantics engineering for Lua 5.2 ⋮ Polymorphic lambda calculus with context-free session types ⋮ Minimal type inference for linked data consumers ⋮ Soundness Conditions for Big-Step Semantics ⋮ ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Unnamed Item ⋮ Combining Model Checking and Data-Flow Analysis ⋮ The Negligible and Yet Subtle Cost of Pattern Matching ⋮ Typed Relational Conversion ⋮ New ⋮ A Realizability Interpretation for Intersection and Union Types ⋮ Unified Syntax with Iso-types ⋮ The HOL-Omega Logic ⋮ Subtyping Supports Safe Session Substitution ⋮ The Recursive Union of Some Gradual Types ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ Computation semantics of the functional scientific workflow language Cuneiform ⋮ A programming model and foundation for lineage-based distributed computation ⋮ An extended account of contract monitoring strategies as patterns of communication ⋮ Push versus pull-based loop fusion in query engines ⋮ Environment classifiers ⋮ Bigraphs and transitions ⋮ The m-calculus ⋮ A generic approach to the static analysis of concurrent programs with procedures ⋮ Discovering affine equalities using random interpretation ⋮ Bitwidth aware global register allocation ⋮ Folklore confirmed ⋮ New results on the computability and complexity of points--to analysis ⋮ Incremental algorithms for dispatching in dynamically typed languages ⋮ From control effects to typed continuation passing ⋮ Coercive subtyping for the calculus of constructions ⋮ A type theory for memory allocation and data layout ⋮ Static prediction of heap space usage for first-order functional programs ⋮ Ownership types for object encapsulation ⋮ Guarded recursive datatype constructors ⋮ A type system for higher-order modules ⋮ Pure patterns type systems ⋮ Fairness and communication-based semantics for session-typed languages ⋮ Extensional Logic of Hyperintensions ⋮ Call-by-Value Is Dual to Call-by-Name, Extended ⋮ Realist Consequence, Epistemic Inference, Computational Correctness ⋮ αCheck: A mechanized metatheory model checker ⋮ In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Many more predecessors: A representation workout ⋮ Программное обеспечение для моделирования флюидодинамики и трансфазных процессов в коллекторах, содержащих газогидраты ⋮ Unnamed Item ⋮ Gradual type-and-effect systems ⋮ No value restriction is needed for algebraic effects and handlers ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report) ⋮ A Light Modality for Recursion ⋮ The Essence of Functional Programming on Semantic Data ⋮ $$\mathsf {qPCF}$$ : A Language for Quantum Circuit Computations ⋮ Syntactic Metatheory of Higher-Order Subtyping ⋮ A formal language for cyclic operads ⋮ A Calculus for Language Transformations ⋮ A Type Theory for Probabilistic $$\lambda $$–calculus ⋮ Typing Local Control and State Using Flow Analysis ⋮ A New Method for Dependent Parsing ⋮ Generic Authenticated Data Structures, Formally. ⋮ MikiBeta : A General GUI Library for Visualizing Proof Trees ⋮ Termination checking with types ⋮ Memory Policy Analysis for Semantics Specifications in Maude ⋮ Asynchronous Session Types and Progress for Object Oriented Languages ⋮ An Introduction to the Lambda Calculus ⋮ Introduction to Type Theory ⋮ Extended Static Checking by Calculation Using the Pointfree Transform ⋮ Unifying Sets and Programs via Dependent Types ⋮ onlineSPARC: A Programming Environment for Answer Set Programming ⋮ Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions ⋮ A Language for Biochemical Systems: Design and Formal Specification ⋮ A Transformational Approach to Resource Analysis with Typed-norms Inference ⋮ Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types ⋮ Reasoning in Abella about Structural Operational Semantics Specifications ⋮ Categories of Timed Stochastic Relations ⋮ Unnamed Item ⋮ Implicit Propagation in Structural Operational Semantics ⋮ Unnamed Item ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ COCHIS: Stable and coherent implicits ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Full Abstraction in a Subtyped pi-Calculus with Linear Types ⋮ A Gentle Introduction to Multiparty Asynchronous Session Types ⋮ A Type System for Usage of Software Components ⋮ Probabilistic Analysis of Binary Sessions ⋮ A Type Theory for Robust Failure Handling in Distributed Systems ⋮ PiStache: Implementing π-Calculus in Scala ⋮ Intersection, Universally Quantified, and Reference Types ⋮ A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References ⋮ Concurrent Reversible Sessions ⋮ A Calculus of Global Interaction based on Session Types ⋮ A Parametric Calculus for Mobile Open Code ⋮ Rule-Based Operational Semantics for an Imperative Language ⋮ Linear capabilities for fully abstract compilation of separation-logic-verified code ⋮ Blame and coercion: Together again for the first time ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract) ⋮ An Institutional Theory for #-Components ⋮ Semantics and Efficient Simulation Algorithms of an Expressive Multilevel Modeling Language ⋮ Type-based analysis of logarithmic amortised complexity ⋮ Applied Choreographies ⋮ Precise Subtyping for Asynchronous Multiparty Sessions ⋮ ElixirST: a session-based type system for elixir modules ⋮ Programming language semantics: It’s easy as 1,2,3 ⋮ DNAQL: a query language for DNA sticker complexes ⋮ Functional choreographic programming ⋮ Type inference for rank-2 intersection types using set unification ⋮ A sound strategy to compile general recursion into finite depth pattern matching ⋮ The different shades of infinite session types ⋮ Lifting numeric relational domains to algebraic data types ⋮ Extracting total Amb programs from proofs ⋮ Polarized subtyping ⋮ On Jacobson’s “Towards a Variable-Free Semantics” ⋮ Partially Typed Multiparty Sessions ⋮ Unnamed Item ⋮ An introduction to algebraic effects and handlers (invited tutorial paper) ⋮ A type-based analysis of causality loops in hybrid systems modelers ⋮ Efficient algorithms for isomorphisms of simple types
Uses Software
