Normalisation by evaluation for dependent types

QR Code

Normalisation by evaluation for dependent types

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction. NBE for simple types is u...

Full description

Bibliographic Details
Main Authors:	Altenkirch, Thorsten, Kaposi, Ambrus
Format:	Conference or Workshop Item
Published:	2016
Subjects:	Normalisation by evaluation dependent types internal type theory logical relations Agda
Online Access:	https://eprints.nottingham.ac.uk/34287/

Similar Items

Normalisation by evaluation for type theory, in type theory
by: Altenkirch, Thorsten, et al.
Published: (2017)

Type theory in type theory using quotient inductive types
by: Altenkirch, Thorsten, et al.
Published: (2016)

Type theory in a type theory with quotient inductive types
by: Kaposi, Ambrus
Published: (2017)

Towards a cubical type theory without an interval
by: Altenkirch, Thorsten, et al.
Published: (2017)

Types with extra structure: predicates, equations, composition
by: Hewer, Brandon
Published: (2024)

Bootstrapping extensionality
by: Sestini, Filippo
Published: (2023)

Extending homotopy type theory with strict equality
by: Altenkirch, Thorsten, et al.
Published: (2016)

Partiality, revisited: the partiality monad as a quotient inductive-inductive type
by: Altenkirch, Thorsten, et al.
Published: (2017)

Quotient types in type theory
by: Li, Nuo
Published: (2015)

Agent-Based Logics in Dependent Type Theory
by: Baston, Colm
Published: (2025)

Notions of anonymous existence in Martin-Löf type theory
by: Kraus, Nicolai, et al.
Published: (2016)

Higher inductive types, inductive families, and inductive-inductive types
by: von Raumer, Jakob
Published: (2020)

A framework for relating, implementing and verifying argumentation models and their translations
by: van Gijzel, Bas
Published: (2016)

Learning of interval and general type-2 fuzzy logic systems using simulated annealing: theory and practice
by: Almaraashia, M., et al.
Published: (2016)

Handling uncertainty: from type-1 to interval type-2 fuzzy sets and systems
by: Aladi, Jabran
Published: (2016)

Constructions with non-recursive higher inductive types
by: Kraus, Nicolai
Published: (2016)

Effectiveness of a nurse-led diabetes self-management education on glycosylated hemoglobin among Iranian adults with type 2 diabetes
by: Azami, Golnaz
Published: (2019)

Truncation levels in homotopy type theory
by: Kraus, Nicolai
Published: (2015)

Effect of Diet, Insulin and Exercise on the Regulation of Carbohydrate Metabolism in Health and Type 1 Diabetes
by: Chokkalingam, Kamalakkannan
Published: (2007)

Exploring the micro-politics of normalisation: Narratives of pleasure, self-control and desire in a sample of young Australian ‘party drug’ users
by: Pennay, Amy, et al.
Published: (2010)

Interval type-2 fuzzy modelling and stochastic search for real-world inventory management
by: Miller, Simon, et al.
Published: (2012)

Influence of vegetation and soil types on the wheatbelt termite, Drepanotermes tamminensis (Hill), in the Western Australian wheatbelt
by: Park, H., et al.
Published: (1994)

On Nie-Tan operator and type-reduction of interval type-2 fuzzy sets
by: Li, Jiawei, et al.
Published: (2018)

Baroque Historical Dances Lecture and Workshop by Mireia Frutos Fernandez : World Music History Lecture Series
by: Universiti Teknologi MARA, Faculty of Music
Published: (2018)

Some constructions on ω-groupoids
by: Altenkirch, Thorsten, et al.
Published: (2014)

Evaluation of pre-diploma students using fuzzy approach / Zamali Tarmudi, Mazalan Sarahintu and Ajis Lepit
by: Tarmudi, Zamali, et al.
Published: (2015)

Analysis of g s-transferase, protien tyrosine phosphatase 1B, nuclear factor kappa-B1 and leptin receptor genetic polymorphisms as risk factors for Malaysian type 2 diabetes mellitus subjects
by: Etemad, Ali
Published: (2013)

A Study on Relationship Between Decision-making Behaviour and Myers-Briggs Type Indicator
by: Chen, Jelico
Published: (2007)

Interval type-2 A-intuitionistic fuzzy logic for regression problems
by: Eyoh, Imo, et al.
Published: (2017)

Towards safe and efficient functional reactive programming
by: Sculthorpe, Neil
Published: (2011)

Factors associated with glycaemic control among diabetes mellitus type 2 patients attending health clinics in Tampin district Negeri Sembilan, Malaysia
by: Wan Hamdzan, Wan Farzana Fasya
Published: (2016)

A novel framework for the implementation and evaluation of type-1 and interval type-2 ANFIS
by: Chen, Chao
Published: (2018)

Study of bandgap property of a bilayer membrane-type metamaterial applied on a thin plate
by: GAO, Cong, et al.
Published: (2020)

Interval type-2 intuitionistic fuzzy logic systems - a comparative evaluation
by: Eyoh, Imo, et al.
Published: (2018)

Improving security requirements adequacy: an interval type 2 fuzzy logic security assessment system
by: Hibshi, Hanan, et al.
Published: (2016)

Type-2 fuzzy linear systems
by: Najariyan, Marzieh, et al.
Published: (2017)

The role of C-type lectin receptors in the recognition of Pseudiminas aeruginosa
by: Alshahrani, Mohammad
Published: (2018)

The power of normalised word vectors for automatically grading essays
by: Williams, Robert
Published: (2006)

Prediction of bandgaps in membrane-type metamaterial attached to a thin plate
by: Gao, Cong, et al.
Published: (2019)

Assisted query formulation using normalised word vector and dynamic ontological filtering
by: Dreher, Heinz, et al.
Published: (2006)