Patricia Johann

Pierre Cagne

CoRR, 2022

(Deep) induction rules for GADTs.

[BibT_eX]

[DOI]

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

Characterizing Functions Mappable over GADTs.

[BibT_eX]

[DOI]

Pierre Cagne

Proceedings of the Programming Languages and Systems - 20th Asian Symposium, 2022

2021

Parametricity for Nested Types and GADTs.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2021

(Deep) Induction Rules for GADTs.

[BibT_eX]

[DOI]

CoRR, 2021

GADTs, Functoriality, Parametricity: Pick Two.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 16th Logical and Semantic Frameworks with Applications, 2021

Parametricity for Nested Types and GADTs.

[BibT_eX]

[DOI]

CoRR, 2021

Parametricity for Primitive Nested Types.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2021

2020

Local Presentability of Certain Comma Categories.

[BibT_eX]

[DOI]

Appl. Categorical Struct., 2020

Preface.

[BibT_eX]

[DOI]

Proceedings of the 36th Conference on the Mathematical Foundations of Programming Semantics, 2020

Deep Induction: Induction Rules for (Truly) Nested Types.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2020

2019

Higher-Kinded Data Types: Syntax and Semantics.

[BibT_eX]

[DOI]

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

2018

On local presentability of T/A.

[BibT_eX]

[DOI]

CoRR, 2018

A General Framework for Relational Parametricity.

[BibT_eX]

[DOI]

Kristina Sojakova

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

Cubical Categories for Higher-Dimensional Parametricity.

[BibT_eX]

[DOI]

Kristina Sojakova

CoRR, 2017

2016

A Productivity Checker for Logic Programming.

[BibT_eX]

[DOI]

Ekaterina Komendantskaya

Martin Schmidt

Proceedings of the Logic-Based Program Synthesis and Transformation, 2016

2015

Interleaving data and effects.

[BibT_eX]

[DOI]

J. Funct. Program., 2015

Bifibrational Functorial Semantics of Parametric Polymorphism.

[BibT_eX]

[DOI]

Fredrik Nordvall Forsberg

Federico Orsanigo

Tim Revell

Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, 2015

Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic.

[BibT_eX]

[DOI]

Ekaterina Komendantskaya

CoRR, 2015

Structural Resolution for Logic Programming.

[BibT_eX]

[DOI]

Ekaterina Komendantskaya

Vladimir Komendantskiy

Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, August 31, 2015

2014

A relationally parametric model of dependent type theory.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013

Indexed Induction and Coinduction, Fibrationally.

[BibT_eX]

[DOI]

Clément Fumex

Log. Methods Comput. Sci., 2013

Abstraction and invariance for algebraically indexed types.

[BibT_eX]

[DOI]

Andrew Kennedy

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

2012

Generic Fibrational Induction

[BibT_eX]

[DOI]

Clément Fumex

Log. Methods Comput. Sci., 2012

Refining Inductive Types

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Fibrational Induction Meets Effects.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2012

2011

When Is a Type Refinement an Inductive Type?

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2011

2010

A Generic Operational Metatheory for Algebraic Effects.

[BibT_eX]

[DOI]

Alex Simpson

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

Fibrational Induction Rules for Initial Algebras.

[BibT_eX]

[DOI]

Clément Fumex

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

A principled approach to programming with nested types in Haskell.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2009

A family of syntactic logical relations for the semantics of Haskell-like languages.

[BibT_eX]

[DOI]

Inf. Comput., 2009

2008

Short Cut Fusion for Effects.

[BibT_eX]

Proceedings of the Nineth Symposium on Trends in Functional Programming, 2008

Foundations for structured programming with GADTs.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

2007

Selective strictness and parametricity in structural operational semantics, inequationally.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

Monadic augment and generalised short cut fusion.

[BibT_eX]

[DOI]

J. Funct. Program., 2007

Initial Algebra Semantics Is Enough!

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

2006

The Impact of seq on Free Theorems-Based Program Transformations.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2006

2005

On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2005

Monadic augment and generalised short cut fusion.

[BibT_eX]

[DOI]

Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

2004

Free theorems in the presence of <i>seq</i>.

[BibT_eX]

[DOI]

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

2003

Short cut fusion is correct.

[BibT_eX]

[DOI]

J. Funct. Program., 2003

Staged Notational Definitions.

[BibT_eX]

[DOI]

Walid Taha

Proceedings of the Generative Programming and Component Engineering, 2003

2002

A Generalization of Short-Cut Fusion and its Correctness Proof.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2002

2001

Fusing Logic and Control with Local Transformations: An Example Optimization.

[BibT_eX]

[DOI]

Eelco Visser

Proceedings of the 1st International Workshop on Reduction Strategies in Rewriting and Programming, 2001

Lumberjack Summer Camp: A Cross-Institutional Undergraduate Research Experience in Computer Science.

[BibT_eX]

[DOI]

Franklyn A. Turbak

Comput. Sci. Educ., 2001

Short Cut Fusion: Proved and Improved.

[BibT_eX]

[DOI]

Proceedings of the Semantics, 2001

2000

Testing and enhancing a prototype program fusion engine.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 2000

Warm fusion in Stratego: A case study in generation of program transformation systems.

[BibT_eX]

[DOI]

Eelco Visser

Ann. Math. Artif. Intell., 2000

1999

A funny thing happened on the way to the formula: demonstrating equality of functions and programs.

[BibT_eX]

[DOI]

Proceedings of the Working Group Reports from ITiCSE on Innovation and Technology in Computer Science Education, 1999

1997

Deduction systems.

[BibT_eX]

[DOI]

Rolf Socher-Ambrosius

Graduate Texts in Computer Science, Springer, ISBN: 978-1-4612-2266-8, 1997

1995

A Combinatory Logic Approach to Higher-Order E-Unification.

[BibT_eX]

[DOI]

Daniel J. Dougherty

Theor. Comput. Sci., 1995

1994

Normal Forms in Combinatory Logic.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 1994

Solving Simplification Ordering Constraints.

[BibT_eX]

[DOI]

Rolf Socher-Ambrosius

Proceedings of the Constraints in Computational Logics, First International Conference, 1994

Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading.

[BibT_eX]

[DOI]

Michael Kohlhase

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1992

An Improved General E-Unification Method.

[BibT_eX]

[DOI]

Daniel J. Dougherty

J. Symb. Comput., 1992

A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract).

[BibT_eX]

[DOI]

Daniel J. Dougherty