Using dependent types to express modular structure

No abstract is available for this paper.

• Publication year

  1986

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  Unknown publication date

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/512644.512670
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Persistence and Type Abstraction

  1988cited by this paper
• "Type" is not a type

  1986cited by this paper
• Representation independence and data abstraction

  1986cited by this paper
• Abstract types have existential types

  1985influential reference
• On understanding types, data abstraction, and polymorphism

  1985cited by this paper
• Data types are values

  1985cited by this paper
• Constructive mathematics and computer programming

  1984cited by this paper
• Modules for standard ML

  1984cited by this paper
• Understanding Russell- A First Attempt

  1984cited by this paper
• Programming with Modules as Typed Functional Programming

  1984cited by this paper
• A Kernel Language for Abstract Data Types and Modules

  1984influential reference
• The Type Theory of PL/CV3

  1981influential reference
• To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism

  1980cited by this paper
• An Informal Description of Russell

  1980cited by this paper
• An investigation of a programming language with a polymorphic type structure.

  1979cited by this paper
• A Theory of Type Polymorphism in Programming

  1978cited by this paper
• Combinatory logic

  1977influential reference
• An Intuitionistic Theory of Types: Predicative Part

  1975cited by this paper
• Towards a theory of type structure

  1974cited by this paper
• Une Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des Types

  1971cited by this paper
• Symposium on Automatic Demonstration

  1970cited by this paper

• Avoiding Signature Avoidance in ML Modules with Zippers

  2025cites this paper
• Extensibility in Programming Languages: An overview

  2025cites this paper
• Fulfilling OCaml Modules with Transparency

  2024cites this paper
• Fulfilling OCaml modules with transparent existentials

  2023cites this paper
• Fulfilling OCaml modules with transparent existentials

  2023cites this paper
• Reflections on existential types

  2022cites this paper
• An existential crisis resolved: type inference for first-class existential types

  2021cites this paper
• Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification

  2021cites this paper
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

  2020cites this paper
• The history of Standard ML

  2020cites this paper
• Fully abstract module compilation

  2019cites this paper
• QED at Large: A Survey of Engineering of Formally Verified Software

  2019cites this paper
• Programming With Structures, Functions, and Objects

  2018cites this paper
• 1ML – Core and modules united

  2018cites this paper
• Type soundness proofs with definitional interpreters

  2017cites this paper
• Static Type Inference for Parametric Classes

  2016cites this paper
• Type soundness for dependent object types (DOT)

  2016cites this paper
• The Essence of Dependent Object Types

  2016cites this paper
• Polymorphism And Type Inference In Database Programming MS-CIS-90-64 LOGIC & COMPUTATION 23

  2016cites this paper
• From F to DOT: Type Soundness Proofs with Definitional Interpreters

  2015cites this paper
• 1ML – core and modules united (F-ing first-class modules)

  2015cites this paper
• Case Studies in Proof Checking

  2014cites this paper
• Verifying Concurrent Programs by Controlling Alias Interference

  2014cites this paper
• Static Type Inference for Parametric Classes

  2014cites this paper
• Foundations of path-dependent types

  2014cites this paper
• Typing artifacts in megamodeling

  2013cites this paper
• Max-planck-institut F ¨ Ur Informatik Metalogical Frameworks I N F O R M a T I K Authors' Addresses Publication Notes

  2013cites this paper
• Practical Foundations for Programming Languages: Type Safety

  2012cites this paper
• Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types. (Programmer avec des modules de première classe dans un langage noyau pourvu de sous-typage, sortes singletons et types existentiels ouverts)

  2010cites this paper
• Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq. (Modular development of theories and name-space management for the Coq proof assistant)

  2010cites this paper
• Pure subtype systems

  2010cites this paper
• Incorporating record subtyping into a relational data model

  2010cites this paper
• A theory of dependent record types with structural subtyping

  2010cites this paper
• True Higher-Order Modules , Separate Compilation , and Signature Calculi ∗

  2009cites this paper
• Sous-typage coercitif en présence de réductions non-standards dans un système aux types dépendants. (Coercive subtyping in a system with dependents types and non-standards reductions)

  2009cites this paper
• Engineering Higher-Order Modules in SML/NJ

  2009cites this paper
• An Extension of ML with First-Class Abstract Types

  2009influential citation
• A Simple and General Theoretical Account for Abstract Types

  2009cites this paper
• ML Modules and Haskell Type Classes: A Constructive Comparison

  2008cites this paper
• Formalizing non-interference for a simple bytecode language in Coq

  2008cites this paper
• Design Concepts in Programming Languages

  2008cites this paper
• Towards a Simpler Account of Modules and Generativity : Abstract Types have Open Existential Types . Benoı̂t Montagu INRIA

  2008cites this paper
• Towards a Simpler Account of Modules and Generativity : Abstract Types have Open Existential Types

  2008cites this paper
• Mei-A Module System for Mechanized Mathematics Systems

  2008cites this paper
• Dynamic Translucency with Abstraction Kinds

  2008cites this paper
• Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions

  2008cites this paper
• Irrelevance, polymorphism, and erasure in type theory

  2008cites this paper
• Abstract Predicates and Mutable ADTs in Hoare Type Theory

  2007cites this paper
• Standard Ml Type Generativity as Existential Quantiication Standard Ml Type Generativity as Existential Quantiication

  2007cites this paper
• Max-planck-institut F Ur Informatik Metalogical Frameworks K I N F O R M a T I K Im Stadtwald D 66123 Saarbr Ucken Germany Authors' Addresses Publication Notes

  2007cites this paper
• A Multiparadigmatic Study of the Object-Oriented Design Patterns

  2007cites this paper
• Logic Column 6 Polymorphism, Objects and Abstract Types

  2007cites this paper
• Typed open programming: a higher-order, typed approach to dynamic modularity and distribution

  2007cites this paper
• Type sharing constraints and undecidability

  2007cites this paper
• First-class polymorphism with existential types

  2006cites this paper
• Understanding and evolving the ml module system

  2005influential citation
• The Open Calculus of Constructions (Part II): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving

  2005cites this paper
• Type Generativity in Higher-Order Module Systems

  2005cites this paper
• A syntactic approach to eta equality in type theory

  2005cites this paper
• The Open Calculus of Constructions (Part I): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving

  2005cites this paper
• Subtype satisfiability and entailment

  2004cites this paper
• Higher-order modules in System F ω and

  2004influential citation
• Types for Modules

  2004influential citation
• Advanced Topics In Types And Programming Languages

  2004cites this paper
• Types and programming languages: the next generation

  2003cites this paper
• A Logical Framework with Dependently Typed Records

  2003cites this paper
• Type systems

  2003cites this paper
• Programming Methodology

  2003cites this paper
• Abstract Data Types Can Have Inequations1

  2003cites this paper
• Typed operational semantics for higher-order subtyping

  2003cites this paper
• A type system for higher-order modules

  2003cites this paper
• Typed Lambda Calculi and Applications

  2003cites this paper
• Type Systems in Programming Languages

  2002cites this paper
• A formal specification of the Haskell 98 module system

  2002cites this paper
• First class modules for Haskell

  2002cites this paper
• Dependently Typed Records in Type Theory

  2002cites this paper
• Thesis Proposal: Effective Type Theory for Modularity

  2002cites this paper
• Type Checking Parametrised Programs and Specifications in ASL+FPC

  2002cites this paper
• Nested Types

  2001cites this paper
• Types in Compilation

  2001influential citation
• From Hindley-Milner Types to First-Class Structures

  2001cites this paper
• Abstraction Barriers and Refinement in the Polymorphic Lambda Calculus

  2001cites this paper
• A Type-based Framework for Automatic Debugging

  2001cites this paper
• Dependent Types with Subtyping and Late-Bound Overloading

  2001cites this paper
• Notes on Programming Standard ML of New Jersey (version 110.0.6)

  2001cites this paper
• Operational Interpretations of an Extension of F ! with Control Operatorsy Capsule Review

  2001cites this paper
• Sharing in Typed Module Assembly Language

  2000cites this paper
• First-Class Structures for Standard ML

  2000cites this paper
• A type-theoretic interpretation of standard ML

  2000cites this paper
• An Introduction to Dependent Type Theory

  2000cites this paper
• Mechanised Formal Reasoning About Modular Programs

  2000cites this paper
• Dependently Typed Records for Representing Mathematical Structure

  2000cites this paper
• Title: Non-dependent Types for Standard Ml Modules Non-dependent Types for Standard Ml Modules

  1999cites this paper
• Interpreting Specialization in Type Theory

  1999cites this paper
• Type Theory & Functional Programming

  1999cites this paper
• Mawl: A Domain-Specific Language for Form-Based Services

  1999cites this paper
• Non-dependent Types for Standard ML Modules

  1999cites this paper
• Transparent modules with fully syntatic signatures

  1999cites this paper
• Typed cross-module compilation

  1998cites this paper
• Polymorphism, objects and abstract types

  1998cites this paper