Extracting ω's programs from proofs in the calculus of constructions

Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '89 ◽

10.1145/75277.75285 ◽

1989 ◽

Cited By ~ 43

Author(s):

C. Paulin-Mohring

Keyword(s):

Calculus Of Constructions

Download Full-text

Soundness of Coercion in the Calculus of Constructions

Journal of Logic and Computation ◽

10.1093/logcom/14.3.405 ◽

2004 ◽

Vol 14 (3) ◽

pp. 405-427 ◽

Cited By ~ 3

Author(s):

G. Chen

Keyword(s):

Calculus Of Constructions

Download Full-text

Coercive subtyping for the calculus of constructions

Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '03 ◽

10.1145/604131.604145 ◽

2003 ◽

Cited By ~ 3

Author(s):

Gang Chen

Keyword(s):

Calculus Of Constructions

Download Full-text

Partial objects in the calculus of constructions

[1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science ◽

10.1109/lics.1991.151633 ◽

2002 ◽

Cited By ~ 3

Author(s):

P. Audebaud

Keyword(s):

Calculus Of Constructions

Download Full-text

Towards Normalization by Evaluation for the βη-Calculus of Constructions

Functional and Logic Programming - Lecture Notes in Computer Science ◽

10.1007/978-3-642-12251-4_17 ◽

2010 ◽

pp. 224-239 ◽

Cited By ~ 4

Author(s):

Andreas Abel

Keyword(s):

Calculus Of Constructions

Download Full-text

Inductively defined types in the Calculus of Constructions

Lecture Notes in Computer Science - Mathematical Foundations of Programming Semantics ◽

10.1007/bfb0040259 ◽

1990 ◽

pp. 209-228 ◽

Cited By ~ 29

Author(s):

Frank Pfenning ◽

Christine Paulin-Mohring

Keyword(s):

Calculus Of Constructions

Download Full-text

Inductive Consequences in the Calculus of Constructions

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-642-14052-5_31 ◽

2010 ◽

pp. 450-465

Author(s):

Daria Walukiewicz-Chrząszcz ◽

Jacek Chrząszcz

Keyword(s):

Calculus Of Constructions

Download Full-text

Computational reflection in the calculus of constructions and its application to theorem proving

Lecture Notes in Computer Science - Typed Lambda Calculi and Applications ◽

10.1007/3-540-62688-3_44 ◽

1997 ◽

pp. 319-335 ◽

Cited By ~ 5

Author(s):

Harald Rueß

Keyword(s):

Theorem Proving ◽

Calculus Of Constructions ◽

Computational Reflection

Download Full-text

A full formalisation of π-calculus theory in the calculus of constructions

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/bfb0028392 ◽

1997 ◽

pp. 153-169 ◽

Cited By ~ 26

Author(s):

Daniel Hirschkoff

Keyword(s):

Calculus Of Constructions ◽

Π Calculus

Download Full-text

Extensionality in the Calculus of Constructions

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/11541868_18 ◽

2005 ◽

pp. 278-293 ◽

Cited By ~ 11

Author(s):

Nicolas Oury

Keyword(s):

Calculus Of Constructions

Download Full-text

The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping

Lecture Notes in Computer Science - Typed Lambda Calculi and Applications ◽

10.1007/3-540-45413-6_27 ◽

2001 ◽

pp. 344-359 ◽

Cited By ~ 36

Author(s):

Alexandre Miquel

Keyword(s):

Type Systems ◽

Pure Type ◽

Calculus Of Constructions ◽

Pure Type Systems

Download Full-text