Gilles Barthe

According to our database1, Gilles Barthe authored at least 191 papers between 1995 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.
PACMPL, 2019

System-Level Non-interference of Constant-Time Cryptography. Part I: Model.
J. Autom. Reasoning, 2019

GALACTICS: Gaussian Sampling for Lattice-Based Constant-Time Implementation of Cryptographic Signatures, Revisited.
IACR Cryptology ePrint Archive, 2019

Bidirectional type checking for relational properties.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

FaCT: a DSL for timing-sensitive computation.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018
Monadic refinements for relational cost analysis.
PACMPL, 2018

Proving expected sensitivity of probabilistic programs.
PACMPL, 2018

maskVerif: a formal tool for analyzing software and hardware masked implementations.
IACR Cryptology ePrint Archive, 2018

Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations.
IACR Cryptology ePrint Archive, 2018

Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences.
Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, 2018

Almost Sure Productivity.
Proceedings of the 45th International Colloquium on Automata, Languages, and Programming, 2018

Masking the GLP Lattice-Based Signature Scheme at Any Order.
Proceedings of the Advances in Cryptology - EUROCRYPT 2018 - 37th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Tel Aviv, Israel, April 29, 2018

An Assertion-Based Program Logic for Probabilistic Programs.
Proceedings of the Programming Languages and Systems, 2018

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.
Proceedings of the Programming Languages and Systems, 2018

Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time".
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks.
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

Symbolic Proofs for Lattice-Based Cryptography.
Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

2017
A relational logic for higher-order programs.
PACMPL, 2017

Provably secure compilation of side-channel countermeasures.
IACR Cryptology ePrint Archive, 2017

A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'.
IACR Cryptology ePrint Archive, 2017

Relational cost analysis.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Coupling proofs are probabilistic product programs.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Proving uniformity and independence by self-composition and coupling.
Proceedings of the LPAR-21, 2017

*-Liftings for Differential Privacy.
Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

Reasoning about Probabilistic Defense Mechanisms against Remote Attacks.
Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
Proceedings of the Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30, 2017

Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs.
Proceedings of the Programming Languages and Systems, 2017

Verified Translation Validation of Static Analyses.
Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

Generic Transformations of Predicate Encodings: Constructions and Applications.
Proceedings of the Advances in Cryptology - CRYPTO 2017, 2017

Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30, 2017

A Fast and Verified Software Stack for Secure Function Evaluation.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30, 2017

Jasmin: High-Assurance and High-Speed Cryptography.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30, 2017

2016
Programming language techniques for differential privacy.
SIGLOG News, 2016

Product programs and relational program logics.
J. Log. Algebr. Meth. Program., 2016

Computer-Aided Verification for Mechanism Design.
Proceedings of the Web and Internet Economics - 12th International Conference, 2016

Verifying Constant-Time Implementations.
Proceedings of the 25th USENIX Security Symposium, 2016

Proving Differential Privacy via Probabilistic Couplings.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Facets of Software Doping.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

A Program Logic for Union Bounds.
Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC.
Proceedings of the Fast Software Encryption - 23rd International Conference, 2016

Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model.
Proceedings of the Advances in Cryptology - EUROCRYPT 2016, 2016

Advanced Probabilistic Couplings for Differential Privacy.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Differentially Private Bayesian Programming.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Strong Non-Interference and Type-Directed Higher-Order Masking.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Synthesizing Probabilistic Invariants via Doob's Decomposition.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
SEFM: software engineering and formal methods.
Software and System Modeling, 2015

High-Assurance Cryptography: Cryptographic Software We Can Trust.
IEEE Security & Privacy, 2015

Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler.
IACR Cryptology ePrint Archive, 2015

Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181).
Dagstuhl Reports, 2015

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds.
Proceedings of the Public-Key Cryptography - PKC 2015 - 18th IACR International Conference on Practice and Theory in Public-Key Cryptography, Gaithersburg, MD, USA, March 30, 2015

Relational Reasoning via Probabilistic Coupling.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols.
Proceedings of the Advances in Cryptology - EUROCRYPT 2015, 2015

Verified Proofs of Higher-Order Masking.
Proceedings of the Advances in Cryptology - EUROCRYPT 2015, 2015

Automated Proofs of Pairing-Based Cryptography.
Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

2014
Formal Verification of an SSA-Based Middle-End for CompCert.
ACM Trans. Program. Lang. Syst., 2014

Verified Implementations for Secure and Verifiable Computation.
IACR Cryptology ePrint Archive, 2014

The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492).
Dagstuhl Reports, 2014

Leakage Resilience against Concurrent Cache Attacks.
Proceedings of the Principles of Security and Trust - Third International Conference, 2014

Probabilistic relational verification for cryptographic implementations.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Proving Differential Privacy in Hoare Logic.
Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Certified Synthesis of Efficient Batch Verifiers.
Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Automated Analysis of Cryptographic Assumptions in Generic Group Models.
Proceedings of the Advances in Cryptology - CRYPTO 2014, 2014

Making RSA-PSS Provably Secure against Non-random Faults.
Proceedings of the Cryptographic Hardware and Embedded Systems - CHES 2014, 2014

Synthesis of Fault Attacks on Cryptographic Implementations.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

System-level Non-interference for Constant-time Cryptography.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

2013
Formally Verified Implementation of an Idealized Model of Virtualization.
Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

Computer-Aided Security Proofs.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

From relational verification to SIMD loop synthesis.
Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2013

Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2013

Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs.
Proceedings of the Automata, Languages, and Programming - 40th International Colloquium, 2013

EasyCrypt: A Tutorial.
Proceedings of the Foundations of Security Analysis and Design VII, 2013

Verified Computational Differential Privacy with Applications to Smart Metering.
Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, 2013

Fully automated analysis of padding-based encryption in the computational model.
Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

2012
Preface.
Journal of Computer Security, 2012

Automated Analysis and Synthesis of Padding-Based Encryption Schemes.
IACR Cryptology ePrint Archive, 2012

Computer-Aided Cryptographic Proofs.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Verified Indifferentiable Hashing into Elliptic Curves.
Proceedings of the Principles of Security and Trust - First International Conference, 2012

Probabilistic relational reasoning for differential privacy.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs.
Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Computer-Aided Cryptographic Proofs.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Secure Multi-Execution through Static Program Transformation.
Proceedings of the Formal Techniques for Distributed Systems, 2012

A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert.
Proceedings of the Programming Languages and Systems, 2012

Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Verified Security of Merkle-Damgård.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

Verified security of redundancy-free encryption from Rabin and RSA.
Proceedings of the ACM Conference on Computer and Communications Security, 2012

Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols.
Proceedings of the ACM Conference on Computer and Communications Security, 2012

2011
An Abstract Model of Certificate Translation.
ACM Trans. Program. Lang. Syst., 2011

Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language.
Proceedings of the Trustworthy Global Computing - 6th International Symposium, 2011

Verifiable Security of Boneh-Franklin Identity-Based Encryption.
Proceedings of the Provable Security - 5th International Conference, 2011

A Computational Indistinguishability Logic for the Bounded Storage Model.
Proceedings of the Foundations and Practice of Security, 2011

Relational Verification Using Product Programs.
Proceedings of the FM 2011: Formal Methods, 2011

Formally Verifying Isolation and Availability in an Idealized Model of Virtualization.
Proceedings of the FM 2011: Formal Methods, 2011

Beyond Provable Security Verifiable IND-CCA Security of OAEP.
Proceedings of the Topics in Cryptology - CT-RSA 2011, 2011

Information-Theoretic Bounds for Differentially Private Mechanisms.
Proceedings of the 24th IEEE Computer Security Foundations Symposium, 2011

Computer-Aided Security Proofs for the Working Cryptographer.
Proceedings of the Advances in Cryptology - CRYPTO 2011, 2011

2010
Perspectives in Certificate Translation.
Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

On the Equality of Probabilistic Terms.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Programming Language Techniques for Cryptographic Proofs.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Functional Framework for Result Checking.
Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

Robustness Guarantees for Anonymity.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

A Machine-Checked Formalization of Sigma-Protocols.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Computational indistinguishability logic.
Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

2009
Formally Certifying the Security of Digital Signature Schemes.
Proceedings of the 30th IEEE Symposium on Security and Privacy (S&P 2009), 2009

Formal certification of code-based cryptographic proofs.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Implementing a Direct Method for Certificate Translation.
Proceedings of the Formal Methods and Software Engineering, 2009

2008
Preservation of Proof Pbligations for Hybrid Verification Methods.
Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

A Tutorial on Type-Based Termination.
Proceedings of the Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24, 2008

Formal Certification of ElGamal Encryption.
Proceedings of the Formal Aspects in Security and Trust, 5th International Workshop, 2008

An Introduction to Certificate Translation.
Proceedings of the Foundations of Security Analysis and Design V, 2008

Certificate translation for specification-preserving advices.
Proceedings of the 7th Workshop on Foundations of Aspect-Oriented Languages, 2008

Certificate Translation in Abstract Interpretation.
Proceedings of the Programming Languages and Systems, 2008

Type-Based Termination with Sized Products.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

Tractable Enforcement of Declassification Policies.
Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

Preservation of Proof Obligations from Java to the Java Virtual Machine.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Certificate Translation.
Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

Certified Reasoning in Memory Hierarchies.
Proceedings of the Programming Languages and Systems, 6th Asian Symposium, 2008

2007
Secure information flow for a concurrent language with scheduling.
Journal of Computer Security, 2007

Security types preserving compilation.
Computer Languages, Systems & Structures, 2007

The MOBIUS Proof Carrying Code Infrastructure.
Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

Security of Multithreaded Programs by Compilation.
Proceedings of the Computer Security, 2007

A Certified Lightweight Non-interference Java Bytecode Verifier.
Proceedings of the Programming Languages and Systems, 2007

07091 Abstracts Collection - Mobility, Ubiquity and Security.
Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

07091 Executive Summary - Mobility, Ubiquity and Security.
Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

2006
Remarks on the equational theory of non-normalizing pure type systems.
J. Funct. Program., 2006

Preventing Timing Leaks Through Transactional Branching Instructions.
Electr. Notes Theor. Comput. Sci., 2006

MOBIUS: Mobility, Ubiquity, Security.
Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

Deriving an Information Flow Checker and Certifying Compiler for Java.
Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P 2006), 2006

Certificate Translation for Optimizing Compilers.
Proceedings of the Static Analysis, 13th International Symposium, 2006

CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions.
Proceedings of the Logic for Programming, 2006

JACK - A Tool for Validation of Security and Behaviour of Java Applications.
Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.
Proceedings of the Functional and Logic Programming, 8th International Symposium, 2006

2005
A computational view of implicit coercions in type theory.
Mathematical Structures in Computer Science, 2005

Tool-Assisted Specification and Verification of Typed Low-Level Languages.
J. Autom. Reasoning, 2005

Non-interference for a JVM-like language.
Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

Practical Inference for Type-Based Termination in a Polymorphic Setting.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Precise Analysis of Memory Consumption using Program Logics.
Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Proof Obligations Preserving Compilation.
Proceedings of the Formal Aspects in Security and Trust, Third International Workshop, 2005

Formal Methods for Smartcard Security.
Proceedings of the Foundations of Security Analysis and Design III, 2005

2004
Type-based termination of recursive definitions.
Mathematical Structures in Computer Science, 2004

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming.
J. Funct. Program., 2004

Security Types Preserving Compilation: (Extended Abstract).
Proceedings of the Verification, 2004

A Machine-Checked Formalization of the Random Oracle Model.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

A Tool-Assisted Framework for Certified Bytecode Verification.
Proceedings of the Fundamental Approaches to Software Engineering, 2004

Secure Information Flow by Self-Composition.
Proceedings of the 17th IEEE Computer Security Foundations Workshop, 2004

Formally verifying information flow type systems for concurrent and thread systems.
Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, 2004

Enforcing High-Level Security Properties for Applets.
Proceedings of the Smart Card Research and Advanced Applications VI, 2004

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Setoids in type theory.
J. Funct. Program., 2003

Validation of the JavaCard Platform with Implicit Induction Techniques.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Pure patterns type systems.
Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

2002
Preface.
Electr. Notes Theor. Comput. Sci., 2002

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines.
Proceedings of the Verification, 2002

Efficient Reasoning about Executable Specifications in Coq.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

CPS translating inductive and coinductive types.
Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '02), 2002

Compositional Verification of Secure Applet Interactions.
Proceedings of the Fundamental Approaches to Software Engineering, 2002

Tool-Assisted Specification and Verification of the JavaCard Platform.
Proceedings of the Algebraic Methodology and Software Technology, 2002

2001
Weak normalization implies strong normalization in a class of non-dependent pure type systems.
Theor. Comput. Sci., 2001

An induction principle for pure type systems.
Theor. Comput. Sci., 2001

Type Isomorphisms and Proof Reuse in Dependent Type Theory.
Proceedings of the Foundations of Software Science and Computation Structures, 2001

A Formal Executable Semantics of the JavaCard Platform.
Proceedings of the Programming Languages and Systems, 2001

Jakarta: A Toolset for Reasoning about JavaCard.
Proceedings of the Smart Card Programming and Security, 2001

2000
Static Reduction Analysis for Imperative Object Oriented Languages.
Proceedings of the Logic for Programming and Automated Reasoning, 2000

Constructor Subtyping in the Calculus of Inductive Constructions.
Proceedings of the Foundations of Software Science and Computation Structures, 2000

An Introduction to Dependent Type Theory.
Proceedings of the Applied Semantics, International Summer School, 2000

1999
CPS Translations and Applications: The Cube and Beyond.
Higher-Order and Symbolic Computation, 1999

Type-checking injective pure type systems.
J. Funct. Program., 1999

Order-Sorted Inductive Types.
Inf. Comput., 1999

Expanding the Cube.
Proceedings of the Foundations of Software Science and Computation Structure, 1999

Partial Evaluation and Non-interference for Object Calculi.
Proceedings of the Functional and Logic Programming, 4th Fuji International Symposium, 1999

Constructor Subtyping.
Proceedings of the Programming Languages and Systems, 1999

1998
The Semi-Full Closure of Pure Type Systems.
Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

The Relevance of Proof-Irrelevance.
Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion.
Proceedings of the Computer Science Logic, 12th International Workshop, 1998

1997
Monadic Type Systems: Pure Type Systems for Impure Settings.
Electr. Notes Theor. Comput. Sci., 1997

A notion of classical pure type system.
Electr. Notes Theor. Comput. Sci., 1997

Reflections on Reflections.
Proceedings of the Programming Languages: Implementations, 1997

Domain-Free Pure Type Systems.
Proceedings of the Logical Foundations of Computer Science, 4th International Symposium, 1997

Termination of Algebraic Type Systems: The Syntactic Approach.
Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

Explicit Substitutions for the Lambda-Calculus.
Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

1996
Towards Lean Proof Checking.
Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

On the Subject Reduction Property for Algebraic Type Systems.
Proceedings of the Computer Science Logic, 10th International Workshop, 1996

1995
A Two-Level Approach Towards Lean Proof-Checking.
Proceedings of the Types for Proofs and Programs, 1995

Implicit Coercions in Type Systems.
Proceedings of the Types for Proofs and Programs, 1995

Extensions of Pure Type Systems.
Proceedings of the Typed Lambda Calculi and Applications, 1995

Modular Properties of Algebraic Type Systems.
Proceedings of the Higher-Order Algebra, 1995

A Simple Abstract Semantics for Equational Theories.
Proceedings of the Fundamentals of Computation Theory, 10th International Symposium, 1995

Congruence Types.
Proceedings of the Computer Science Logic, 9th International Workshop, 1995


  Loading...